1.1 --- a/src/HOL/Library/Quicksort.thy	Thu Aug 28 15:24:30 2008 +0200
     1.2 +++ b/src/HOL/Library/Quicksort.thy	Thu Aug 28 15:33:33 2008 +0200
     1.3 @@ -12,13 +12,9 @@
     1.4  context linorder
     1.5  begin
     1.6  
     1.7 -function quicksort :: "'a list \<Rightarrow> 'a list" where
     1.8 +fun quicksort :: "'a list \<Rightarrow> 'a list" where
     1.9  "quicksort []     = []" |
    1.10  "quicksort (x#xs) = quicksort([y\<leftarrow>xs. ~ x\<le>y]) @ [x] @ quicksort([y\<leftarrow>xs. x\<le>y])"
    1.11 -by pat_completeness auto
    1.12 -
    1.13 -termination by (relation "measure size")
    1.14 -  (auto simp: length_filter_le [THEN preorder_class.le_less_trans])
    1.15  
    1.16  lemma quicksort_permutes [simp]:
    1.17    "multiset_of (quicksort xs) = multiset_of xs"