diff -r 129d31b162f3 -r 852d6ed1b5c6 src/HOL/Library/Quicksort.thy
--- a/src/HOL/Library/Quicksort.thy	Thu Nov 04 09:53:23 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-(*  Author:     Tobias Nipkow
-    Copyright   1994 TU Muenchen
-*)
-
-header {* Quicksort *}
-
-theory Quicksort
-imports Main Multiset
-begin
-
-context linorder
-begin
-
-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]"
-
-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) (simp_all add: ac_simps)
-
-lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
-  by (simp add: set_count_greater_0)
-
-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
-
-end