--- a/src/HOL/Library/Quicksort.thy Thu Aug 28 15:24:30 2008 +0200
+++ b/src/HOL/Library/Quicksort.thy Thu Aug 28 15:33:33 2008 +0200
@@ -12,13 +12,9 @@
context linorder
begin
-function quicksort :: "'a list \<Rightarrow> 'a list" where
+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])"
-by pat_completeness auto
-
-termination by (relation "measure size")
- (auto simp: length_filter_le [THEN preorder_class.le_less_trans])
lemma quicksort_permutes [simp]:
"multiset_of (quicksort xs) = multiset_of xs"