# HG changeset patch
# User haftmann
# Date 1216980208 -7200
# Node ID 6392b92c3536fac8f8720a4df3246685eb417674
# Parent  85ea2be46c714d5fcdea39fabf28fb6bd898b579
tuned

diff -r 85ea2be46c71 -r 6392b92c3536 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Jul 25 07:35:53 2008 +0200
+++ b/src/HOL/IsaMakefile	Fri Jul 25 12:03:28 2008 +0200
@@ -302,6 +302,7 @@
   Library/Numeral_Type.thy			\
   Library/Boolean_Algebra.thy Library/Countable.thy Library/RType.thy	\
   Library/Heap.thy Library/Heap_Monad.thy Library/Array.thy		\
+  Library/Assert.thy Library/Relational.thy Library/Sublist.thy Library/Subarray.thy	\
   Library/Ref.thy Library/Imperative_HOL.thy Library/RBT.thy		\
   Library/Enum.thy Real/Float.thy $(SRC)/Tools/float.ML
 	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
@@ -769,7 +770,8 @@
   ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
   ex/Sudoku.thy ex/Tarski.thy ex/Unification.thy ex/document/root.bib	\
   ex/document/root.tex ex/Meson_Test.thy ex/reflection.ML ex/set.thy	\
-  ex/svc_funcs.ML ex/svc_test.thy Library/Parity.thy Library/GCD.thy	\
+  ex/svc_funcs.ML ex/svc_test.thy	\
+  ex/ImperativeQuicksort.thy	\
   Complex/ex/BigO_Complex.thy Complex/ex/BinEx.thy			\
   Complex/ex/Sqrt.thy							\
   Complex/ex/Sqrt_Script.thy Complex/ex/MIR.thy Complex/ex/mirtac.ML	\
diff -r 85ea2be46c71 -r 6392b92c3536 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Fri Jul 25 07:35:53 2008 +0200
+++ b/src/HOL/Nat.thy	Fri Jul 25 12:03:28 2008 +0200
@@ -391,19 +391,12 @@
 instance
 proof
   fix n m :: nat
-  have less_imp_le: "n < m \<Longrightarrow> n \<le> m"
-    unfolding less_eq_Suc_le by (erule Suc_leD)
-  have irrefl: "\<not> m < m" by (induct m) auto
-  have strict: "n \<le> m \<Longrightarrow> n \<noteq> m \<Longrightarrow> n < m"
+  show "n < m \<longleftrightarrow> n \<le> m \<and> \<not> m \<le> n" 
   proof (induct n arbitrary: m)
-    case 0 then show ?case
-      by (cases m) (simp_all add: less_eq_Suc_le)
+    case 0 then show ?case by (cases m) (simp_all add: less_eq_Suc_le)
   next
-    case (Suc n) then show ?case
-      by (cases m) (simp_all add: less_eq_Suc_le)
+    case (Suc n) then show ?case by (cases m) (simp_all add: less_eq_Suc_le)
   qed
-  show "n < m \<longleftrightarrow> n \<le> m \<and> n \<noteq> m"
-    by (auto simp add: irrefl intro: less_imp_le strict)
 next
   fix n :: nat show "n \<le> n" by (induct n) simp_all
 next
diff -r 85ea2be46c71 -r 6392b92c3536 src/HOL/ZF/Games.thy
--- a/src/HOL/ZF/Games.thy	Fri Jul 25 07:35:53 2008 +0200
+++ b/src/HOL/ZF/Games.thy	Fri Jul 25 12:03:28 2008 +0200
@@ -926,7 +926,6 @@
 instance Pg :: pordered_ab_group_add 
 proof
   fix a b c :: Pg
-  show "(a < b) = (a \<le> b \<and> a \<noteq> b)" by (simp add: Pg_less_def)
   show "a - b = a + (- b)" by (simp add: Pg_diff_def)
   {
     assume ab: "a \<le> b"
@@ -936,6 +935,7 @@
       apply (simp add: eq_game_def)
       done
   }
+  then show "(a < b) = (a \<le> b \<and> \<not> b \<le> a)" by (auto simp add: Pg_less_def)
   show "a + b = b + a"
     apply (cases a, cases b)
     apply (simp add: eq_game_def plus_game_comm)
diff -r 85ea2be46c71 -r 6392b92c3536 src/HOL/ex/ImperativeQuicksort.thy
--- a/src/HOL/ex/ImperativeQuicksort.thy	Fri Jul 25 07:35:53 2008 +0200
+++ b/src/HOL/ex/ImperativeQuicksort.thy	Fri Jul 25 12:03:28 2008 +0200
@@ -1,4 +1,4 @@
-theory ImperativeQuickSort
+theory ImperativeQuicksort
 imports Imperative_HOL Subarray Multiset Efficient_Nat
 begin
 
diff -r 85ea2be46c71 -r 6392b92c3536 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Fri Jul 25 07:35:53 2008 +0200
+++ b/src/HOL/ex/ROOT.ML	Fri Jul 25 12:03:28 2008 +0200
@@ -6,7 +6,6 @@
 
 no_document use_thys [
   "Parity",
-  "GCD",
   "Eval",
   "State_Monad",
   "Efficient_Nat_examples",
@@ -21,6 +20,7 @@
 no_document use_thy "Codegenerator_Pretty";
 
 use_thys [
+  "ImperativeQuicksort",
   "Higher_Order_Logic",
   "Abstract_NAT",
   "Guess",