diff -r 3d5b2b874e14 -r a73f8a7784bd ex/Qsort.thy
--- a/ex/Qsort.thy	Wed Feb 16 15:13:53 1994 +0100
+++ b/ex/Qsort.thy	Wed Feb 23 10:05:35 1994 +0100
@@ -6,20 +6,12 @@
 Quicksort
 *)
 
-Qsort = List +
+Qsort = Sorting +
 consts
-  sorted :: "[['a,'a] => bool, 'a list] => bool"
-  mset   :: "'a list => ('a => nat)"
   qsort  :: "[['a,'a] => bool, 'a list] => 'a list"
 
 rules
 
-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))"
-
 qsort_Nil  "qsort(le,[]) = []"
 qsort_Cons "qsort(le,Cons(x,xs)) = qsort(le,[y:xs . ~le(x,y)]) @ \
 \                                  Cons(x, qsort(le,[y:xs . le(x,y)]))"