author  paulson 
Fri, 10 Mar 2000 17:52:48 +0100  
changeset 8414  5983668cac15 
parent 1476  608483c2122a 
child 8524  f990040535c9 
permissions  rwrr 
8414  1 
(* Title: HOL/ex/Qsort.thy 
969  2 
ID: $Id$ 
1476  3 
Author: Tobias Nipkow 
969  4 
Copyright 1994 TU Muenchen 
5 

6 
Quicksort 

7 
*) 

8 

9 
Qsort = Sorting + 

8414  10 
consts qsort :: "((['a,'a] => bool) * 'a list) => 'a list" 
969  11 

8414  12 
recdef qsort "measure (size o snd)" 
13 
simpset "simpset() addsimps [less_Suc_eq_le]" 

14 

15 
"qsort(le, []) = []" 

16 

17 
"qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y]) 

18 
@ (x # qsort(le, [y:xs . le x y]))" 

19 

969  20 
end 