--- 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 \
--- 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
--- 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)
--- 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
--- 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",