--- a/src/HOL/ex/Sorting.thy Fri Mar 10 17:52:48 2000 +0100
+++ b/src/HOL/ex/Sorting.thy Fri Mar 10 17:53:16 2000 +0100
@@ -6,13 +6,11 @@
Specification of sorting
*)
-Sorting = List +
+Sorting = Main +
consts
sorted1:: [['a,'a] => bool, 'a list] => bool
sorted :: [['a,'a] => bool, 'a list] => bool
- mset :: 'a list => ('a => nat)
- total :: (['a,'a] => bool) => bool
- transf :: (['a,'a] => bool) => bool
+ multiset :: 'a list => ('a => nat)
primrec
"sorted1 le [] = True"
@@ -24,10 +22,14 @@
"sorted le (x#xs) = ((!y:set xs. le x y) & sorted le xs)"
primrec
- "mset [] y = 0"
- "mset (x#xs) y = (if x=y then Suc(mset xs y) else mset xs y)"
+ "multiset [] y = 0"
+ "multiset (x#xs) y = (if x=y then Suc(multiset xs y) else multiset xs y)"
-defs
-total_def "total r == (!x y. r x y | r y x)"
-transf_def "transf f == (!x y z. f x y & f y z --> f x z)"
+constdefs
+ total :: (['a,'a] => bool) => bool
+ "total r == (ALL x y. r x y | r y x)"
+
+ transf :: (['a,'a] => bool) => bool
+ "transf f == (ALL x y z. f x y & f y z --> f x z)"
+
end