diff -r f04b33ce250f -r a4dc62a46ee4 ex/Sorting.thy
--- a/ex/Sorting.thy	Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-(*  Title: 	HOL/ex/sorting.thy
-    ID:         $Id$
-    Author: 	Tobias Nipkow
-    Copyright   1994 TU Muenchen
-
-Specification 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,y#zs)) = (f(x,y) & sorted1(f,y#zs))"
-
-sorted_Nil "sorted(le,[])"
-sorted_Cons "sorted(le,x#xs) = ((Alls y:xs. le(x,y)) & sorted(le,xs))"
-
-mset_Nil "mset([],y) = 0"
-mset_Cons "mset(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