--- a/src/HOL/Fundamental_Theorem_Algebra.thy Thu Feb 05 15:35:06 2009 +0100
+++ b/src/HOL/Fundamental_Theorem_Algebra.thy Fri Feb 06 00:10:58 2009 +0000
@@ -3,7 +3,7 @@
header{*Fundamental Theorem of Algebra*}
theory Fundamental_Theorem_Algebra
-imports Polynomial Dense_Linear_Order Complex
+imports Polynomial Complex
begin
subsection {* Square root of complex numbers *}
@@ -59,7 +59,8 @@
by (rule of_real_power [symmetric])
lemma real_down2: "(0::real) < d1 \<Longrightarrow> 0 < d2 ==> EX e. 0 < e & e < d1 & e < d2"
- apply ferrack apply arith done
+ apply (rule exI[where x = "min d1 d2 / 2"])
+ by (simp add: field_simps min_def)
text{* The triangle inequality for cmod *}
lemma complex_mod_triangle_sub: "cmod w \<le> cmod (w + z) + norm z"
--- a/src/HOL/Integration.thy Thu Feb 05 15:35:06 2009 +0100
+++ b/src/HOL/Integration.thy Fri Feb 06 00:10:58 2009 +0000
@@ -557,8 +557,8 @@
apply (drule_tac n = m in partition_lt_gen, auto)
apply (frule partition_eq_bound)
apply (drule_tac [2] partition_gt, auto)
-apply (metis dense_linear_order_class.dlo_simps(8) not_less partition_rhs partition_rhs2)
-apply (metis le_less_trans dense_linear_order_class.dlo_simps(8) nat_le_linear partition_eq_bound partition_rhs2)
+apply (metis linear not_less partition_rhs partition_rhs2)
+apply (metis add_diff_inverse diff_is_0_eq le0 le_diff_conv nat_add_commute partition partition_eq_bound partition_rhs real_less_def termination_basic_simps(5))
done
lemma lemma_additivity4_psize_eq:
--- a/src/HOL/Library/Library.thy Thu Feb 05 15:35:06 2009 +0100
+++ b/src/HOL/Library/Library.thy Fri Feb 06 00:10:58 2009 +0000
@@ -15,6 +15,7 @@
Continuity
ContNotDenum
Countable
+ Dense_Linear_Order
Efficient_Nat
Enum
Eval_Witness
--- a/src/HOL/MacLaurin.thy Thu Feb 05 15:35:06 2009 +0100
+++ b/src/HOL/MacLaurin.thy Fri Feb 06 00:10:58 2009 +0000
@@ -6,7 +6,7 @@
header{*MacLaurin Series*}
theory MacLaurin
-imports Dense_Linear_Order Transcendental
+imports Transcendental
begin
subsection{*Maclaurin's Theorem with Lagrange Form of Remainder*}
--- a/src/HOL/PReal.thy Thu Feb 05 15:35:06 2009 +0100
+++ b/src/HOL/PReal.thy Fri Feb 06 00:10:58 2009 +0000
@@ -9,7 +9,7 @@
header {* Positive real numbers *}
theory PReal
-imports Rational Dense_Linear_Order
+imports Rational
begin
text{*Could be generalized and moved to @{text Ring_and_Field}*}
@@ -22,6 +22,11 @@
A < {r. 0 < r} &
(\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u))))"
+lemma interval_empty_iff:
+ "{y. (x::'a::dense_linear_order) < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
+ by (auto dest: dense)
+
+
lemma cut_of_rat:
assumes q: "0 < q" shows "cut {r::rat. 0 < r & r < q}" (is "cut ?A")
proof -
--- a/src/HOL/Reflection/Ferrack.thy Thu Feb 05 15:35:06 2009 +0100
+++ b/src/HOL/Reflection/Ferrack.thy Fri Feb 06 00:10:58 2009 +0000
@@ -3,7 +3,7 @@
*)
theory Ferrack
-imports Complex_Main Efficient_Nat
+imports Complex_Main Dense_linear_Order Efficient_Nat
uses ("ferrack_tac.ML")
begin
--- a/src/HOL/Reflection/MIR.thy Thu Feb 05 15:35:06 2009 +0100
+++ b/src/HOL/Reflection/MIR.thy Fri Feb 06 00:10:58 2009 +0000
@@ -3,7 +3,7 @@
*)
theory MIR
-imports Complex_Main Efficient_Nat
+imports Complex_Main Dense_Linear_Order Efficient_Nat
uses ("mir_tac.ML")
begin