diff -r 322d065ebef7 -r a680ce27aa56 src/HOL/Library/Quicksort.thy
--- a/src/HOL/Library/Quicksort.thy	Sat May 22 10:12:49 2010 +0200
+++ b/src/HOL/Library/Quicksort.thy	Sat May 22 10:12:50 2010 +0200
@@ -2,7 +2,7 @@
     Copyright   1994 TU Muenchen
 *)
 
-header{*Quicksort*}
+header {* Quicksort *}
 
 theory Quicksort
 imports Main Multiset
@@ -12,22 +12,27 @@
 begin
 
 fun quicksort :: "'a list \<Rightarrow> 'a list" where
-"quicksort []     = []" |
-"quicksort (x#xs) = quicksort([y\<leftarrow>xs. ~ x\<le>y]) @ [x] @ quicksort([y\<leftarrow>xs. x\<le>y])"
+  "quicksort []     = []"
+| "quicksort (x#xs) = quicksort [y\<leftarrow>xs. \<not> x\<le>y] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
+
+lemma [code]:
+  "quicksort []     = []"
+  "quicksort (x#xs) = quicksort [y\<leftarrow>xs. y<x] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
+  by (simp_all add: not_le)
 
 lemma quicksort_permutes [simp]:
   "multiset_of (quicksort xs) = multiset_of xs"
-by (induct xs rule: quicksort.induct) (auto simp: union_ac)
+  by (induct xs rule: quicksort.induct) (simp_all add: ac_simps)
 
 lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
-by(simp add: set_count_greater_0)
+  by (simp add: set_count_greater_0)
 
-lemma sorted_quicksort: "sorted(quicksort xs)"
-apply (induct xs rule: quicksort.induct)
- apply simp
-apply (simp add:sorted_Cons sorted_append not_le less_imp_le)
-apply (metis leD le_cases le_less_trans)
-done
+lemma sorted_quicksort: "sorted (quicksort xs)"
+  by (induct xs rule: quicksort.induct) (auto simp add: sorted_Cons sorted_append not_le less_imp_le)
+
+theorem quicksort_sort [code_unfold]:
+  "sort = quicksort"
+  by (rule ext, rule properties_for_sort) (fact quicksort_permutes sorted_quicksort)+
 
 end