| changeset 3465 | e85c24717cad |
| parent 2517 | 2af078382853 |
| child 5184 | 9b8547a9496a |
--- a/src/HOL/ex/Sorting.thy Thu Jun 26 11:58:05 1997 +0200 +++ b/src/HOL/ex/Sorting.thy Thu Jun 26 13:20:50 1997 +0200 @@ -21,7 +21,7 @@ primrec sorted list "sorted le [] = True" - "sorted le (x#xs) = ((!y:set_of_list xs. le x y) & sorted le xs)" + "sorted le (x#xs) = ((!y:set xs. le x y) & sorted le xs)" primrec mset list "mset [] y = 0"