--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Qsort.thy Wed Mar 22 12:42:34 1995 +0100
@@ -0,0 +1,27 @@
+(* 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