--- 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