diff -r f04b33ce250f -r a4dc62a46ee4 ex/Qsort.thy
--- a/ex/Qsort.thy	Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-(*  Title: 	HOL/ex/qsort.thy
-    ID:         $Id$
-    Author: 	Tobias Nipkow
-    Copyright   1994 TU Muenchen
-
-Quicksort
-*)
-
-Qsort = Sorting +
-consts
-  qsort  :: "[['a,'a] => bool, 'a list] => 'a list"
-
-rules
-
-qsort_Nil  "qsort(le,[]) = []"
-qsort_Cons "qsort(le,x#xs) = qsort(le,[y:xs . ~le(x,y)]) @ 
-                            (x# qsort(le,[y:xs . le(x,y)]))"
-
-(* computational induction.
-   The dependence of p on x but not xs is intentional.
-*)
-qsort_ind
- "[| P([]); 
-    !!x xs. [| P([y:xs . ~p(x,y)]); P([y:xs . p(x,y)]) |] ==> 
-            P(x#xs) |] 
- ==> P(xs)"
-end