diff -r 3d5b2b874e14 -r a73f8a7784bd ex/Sorting.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/Sorting.thy	Wed Feb 23 10:05:35 1994 +0100
@@ -0,0 +1,31 @@
+(*  Title: 	HOL/ex/sorting.thy
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1994 TU Muenchen
+
+Specifikation of sorting
+*)
+
+Sorting = List +
+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"
+
+rules
+
+sorted1_Nil  "sorted1(f,[])"
+sorted1_One  "sorted1(f,[x])"
+sorted1_Cons "sorted1(f,Cons(x,Cons(y,zs))) = (f(x,y) & sorted1(f,Cons(y,zs)))"
+
+sorted_Nil "sorted(le,[])"
+sorted_Cons "sorted(le,Cons(x,xs)) = ((Alls y:xs. le(x,y)) & sorted(le,xs))"
+
+mset_Nil "mset([],y) = 0"
+mset_Cons "mset(Cons(x,xs),y) = if(x=y, Suc(mset(xs,y)), mset(xs,y))"
+
+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))"
+end