instantiation list :: (order) order
begin
fun le_list :: "('a::order)list => 'a list => bool" where
"le_list [] [] = True" |
"le_list (x#xs) (y#ys) = (x <= y & xs <= ys)" |
"le_list _ _ = False"*** exception Empty raised (line 331 of "library.ML") Of course it should be less_eq instead of le, but still... Tobias _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
