# HG changeset patch
# User paulson
# Date 1079689806 -3600
# Node ID 758e7acdea2f3f0764ac5dae9b23e73aa501f09d
# Parent  aa973ba84f69b363a7e651bc037d57a51fd5e024
removed redundant thms

diff -r aa973ba84f69 -r 758e7acdea2f src/HOL/Real/RComplete.thy
--- a/src/HOL/Real/RComplete.thy	Fri Mar 19 10:48:22 2004 +0100
+++ b/src/HOL/Real/RComplete.thy	Fri Mar 19 10:50:06 2004 +0100
@@ -74,7 +74,7 @@
 lemma real_isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::real)"
 apply (frule isLub_isUb)
 apply (frule_tac x = y in isLub_isUb)
-apply (blast intro!: real_le_anti_sym dest!: isLub_le_isUb)
+apply (blast intro!: order_antisym dest!: isLub_le_isUb)
 done
 
 lemma real_order_restrict: "[| (x::real) <=* S'; S <= S' |] ==> x <=* S"
diff -r aa973ba84f69 -r 758e7acdea2f src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Fri Mar 19 10:48:22 2004 +0100
+++ b/src/HOL/Real/RealDef.thy	Fri Mar 19 10:50:06 2004 +0100
@@ -204,9 +204,6 @@
 apply (simp add: real_add preal_add_ac)
 done
 
-lemma real_add_zero_right: "z + (0::real) = z"
-by (simp add: real_add_zero_left real_add_commute)
-
 instance real :: plus_ac0
   by (intro_classes,
       (assumption | 
@@ -634,9 +631,6 @@
      "!!z z'::real. [| w'\<le>w; z'<z |] ==> w' + z' < w + z"
   by (rule Ring_and_Field.add_le_less_mono)
 
-lemma real_zero_less_one: "0 < (1::real)"
-  by (rule Ring_and_Field.zero_less_one)
-
 lemma real_le_square [simp]: "(0::real) \<le> x*x"
  by (rule Ring_and_Field.zero_le_square)
 
@@ -676,12 +670,12 @@
 lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)"
 apply (drule Ring_and_Field.equals_zero_I [THEN sym])
 apply (cut_tac x = y in real_le_square) 
-apply (auto, drule real_le_anti_sym, auto)
+apply (auto, drule order_antisym, auto)
 done
 
 lemma real_sum_squares_cancel2: "x * x + y * y = 0 ==> y = (0::real)"
 apply (rule_tac y = x in real_sum_squares_cancel)
-apply (simp add: real_add_commute)
+apply (simp add: add_commute)
 done
 
 lemma real_add_order: "[| 0 < x; 0 < y |] ==> (0::real) < x + y"
@@ -905,9 +899,6 @@
 lemma real_gt_half_sum: "x < y ==> (x+y)/(2::real) < y"
   by auto
 
-lemma real_dense: "x < y ==> \<exists>r::real. x < r & r < y"
-  by (rule Ring_and_Field.dense)
-
 
 subsection{*Absolute Value Function for the Reals*}
 
@@ -965,7 +956,6 @@
 val real_lbound_gt_zero = thm"real_lbound_gt_zero";
 val real_less_half_sum = thm"real_less_half_sum";
 val real_gt_half_sum = thm"real_gt_half_sum";
-val real_dense = thm"real_dense";
 
 val abs_eqI1 = thm"abs_eqI1";
 val abs_eqI2 = thm"abs_eqI2";
diff -r aa973ba84f69 -r 758e7acdea2f src/HOL/Real/real_arith.ML
--- a/src/HOL/Real/real_arith.ML	Fri Mar 19 10:48:22 2004 +0100
+++ b/src/HOL/Real/real_arith.ML	Fri Mar 19 10:50:06 2004 +0100
@@ -34,7 +34,6 @@
 val real_add_commute = thm"real_add_commute";
 val real_add_assoc = thm"real_add_assoc";
 val real_add_zero_left = thm"real_add_zero_left";
-val real_add_zero_right = thm"real_add_zero_right";
 
 val real_mult = thm"real_mult";
 val real_mult_commute = thm"real_mult_commute";
@@ -54,7 +53,6 @@
 val real_le_refl = thm"real_le_refl";
 val real_le_linear = thm"real_le_linear";
 val real_le_trans = thm"real_le_trans";
-val real_le_anti_sym = thm"real_le_anti_sym";
 val real_less_le = thm"real_less_le";
 val real_less_sum_gt_zero = thm"real_less_sum_gt_zero";
 val real_gt_zero_preal_Ex = thm "real_gt_zero_preal_Ex";
@@ -64,7 +62,6 @@
 val real_less_all_real2 = thm "real_less_all_real2";
 val real_of_preal_le_iff = thm "real_of_preal_le_iff";
 val real_mult_order = thm "real_mult_order";
-val real_zero_less_one = thm "real_zero_less_one";
 val real_add_less_le_mono = thm "real_add_less_le_mono";
 val real_add_le_less_mono = thm "real_add_le_less_mono";
 val real_add_order = thm "real_add_order";