# HG changeset patch
# User wenzelm
# Date 1314719583 -7200
# Node ID 1ad3159323dc816b282781a6dd57cb23314f0bb9
# Parent  a6f9a70d655d3aa67d8c329fbd3913dff29b7dab
tuned import;
discontinued obsolete Sorting.thy (cf. 4d57f872dc2c);

diff -r a6f9a70d655d -r 1ad3159323dc src/HOL/ex/Quicksort.thy
--- a/src/HOL/ex/Quicksort.thy	Tue Aug 30 17:51:30 2011 +0200
+++ b/src/HOL/ex/Quicksort.thy	Tue Aug 30 17:53:03 2011 +0200
@@ -5,7 +5,7 @@
 header {* Quicksort with function package *}
 
 theory Quicksort
-imports Main "~~/src/HOL/Library/Multiset"
+imports "~~/src/HOL/Library/Multiset"
 begin
 
 context linorder
diff -r a6f9a70d655d -r 1ad3159323dc src/HOL/ex/Sorting.thy
--- a/src/HOL/ex/Sorting.thy	Tue Aug 30 17:51:30 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,51 +0,0 @@
-(*  Title:      HOL/ex/Sorting.thy
-    Author:     Tobias Nipkow
-    Copyright   1994 TU Muenchen
-*)
-
-header{*Sorting: Basic Theory*}
-
-theory Sorting
-imports Main "~~/src/HOL/Library/Multiset"
-begin
-
-consts
-  sorted1:: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
-  sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
-
-primrec
-  "sorted1 le [] = True"
-  "sorted1 le (x#xs) = ((case xs of [] => True | y#ys => le x y) &
-                        sorted1 le xs)"
-
-primrec
-  "sorted le [] = True"
-  "sorted le (x#xs) = ((\<forall>y \<in> set xs. le x y) & sorted le xs)"
-
-
-definition
-  total  :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool" where
-   "total r = (\<forall>x y. r x y | r y x)"
-  
-definition
-  transf :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool" where
-   "transf f = (\<forall>x y z. f x y & f y z --> f x z)"
-
-
-
-(* Equivalence of two definitions of `sorted' *)
-
-lemma sorted1_is_sorted: "transf(le) ==> sorted1 le xs = sorted le xs";
-apply(induct xs)
- apply simp
-apply(simp split: list.split)
-apply(unfold transf_def);
-apply(blast)
-done
-
-lemma sorted_append [simp]:
-  "sorted le (xs@ys) = 
-    (sorted le xs & sorted le ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. le x y))"
-  by (induct xs) auto
-
-end