# HG changeset patch
# User krauss
# Date 1219930413 -7200
# Node ID f496e9f343b7aa3caad175388aab136471118a73
# Parent  f47b4af3716a5c4a5ea6199a99ab4009b8920d19
quicksort: function -> fun

diff -r f47b4af3716a -r f496e9f343b7 src/HOL/Library/Quicksort.thy
--- 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"