--- a/src/HOL/ex/Quicksort.thy Tue May 22 14:12:15 2018 +0200
+++ b/src/HOL/ex/Quicksort.thy Tue May 22 11:08:37 2018 +0200
@@ -13,11 +13,11 @@
fun quicksort :: "'a list \<Rightarrow> 'a list" where
"quicksort [] = []"
-| "quicksort (x#xs) = quicksort [y\<leftarrow>xs. \<not> x\<le>y] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
+| "quicksort (x#xs) = quicksort (filter (\<lambda>y. \<not> x\<le>y) xs) @ [x] @ quicksort (filter (\<lambda>y. x\<le>y) xs)"
lemma [code]:
"quicksort [] = []"
- "quicksort (x#xs) = quicksort [y\<leftarrow>xs. y<x] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
+ "quicksort (x#xs) = quicksort (filter (\<lambda>y. \<not> x\<le>y) xs) @ [x] @ quicksort (filter (\<lambda>y. x\<le>y) xs)"
by (simp_all add: not_le)
lemma quicksort_permutes [simp]: