# HG changeset patch
# User paulson
# Date 1109073947 -3600
# Node ID 5f3ef1ddda1fef53992a80e653928c75397a46d2
# Parent  0024472afce7729be07b6a4c8ca6db84cb249d48
removed redundant lemmas and simprules

diff -r 0024472afce7 -r 5f3ef1ddda1f src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Tue Feb 22 10:54:30 2005 +0100
+++ b/src/HOL/Hyperreal/Transcendental.thy	Tue Feb 22 13:05:47 2005 +0100
@@ -158,9 +158,6 @@
 apply (simp add: zero_less_mult_iff)
 done
 
-lemma real_mult_self_eq_zero_iff [simp]: "(r * r = 0) = (r = (0::real))"
-by auto
-
 lemma real_sqrt_gt_zero: "0 < x ==> 0 < sqrt(x)"
 apply (simp add: sqrt_def root_def)
 apply (drule realpow_pos_nth2 [where n=1], safe)
@@ -2222,10 +2219,10 @@
 apply (auto simp add: real_add_commute)
 done
 
-lemma real_sqrt_sum_squares_eq_cancel [simp]: "sqrt(x\<twosuperior> + y\<twosuperior>) = x ==> y = 0"
+lemma real_sqrt_sum_squares_eq_cancel: "sqrt(x\<twosuperior> + y\<twosuperior>) = x ==> y = 0"
 by (drule_tac f = "%x. x\<twosuperior>" in arg_cong, auto)
 
-lemma real_sqrt_sum_squares_eq_cancel2 [simp]: "sqrt(x\<twosuperior> + y\<twosuperior>) = y ==> x = 0"
+lemma real_sqrt_sum_squares_eq_cancel2: "sqrt(x\<twosuperior> + y\<twosuperior>) = y ==> x = 0"
 apply (rule_tac x = y in real_sqrt_sum_squares_eq_cancel)
 apply (simp add: real_add_commute)
 done
@@ -2610,7 +2607,6 @@
 val real_pow_sqrt_eq_sqrt_abs_pow2 = thm "real_pow_sqrt_eq_sqrt_abs_pow2";
 val real_sqrt_pow_abs = thm "real_sqrt_pow_abs";
 val not_real_square_gt_zero = thm "not_real_square_gt_zero";
-val real_mult_self_eq_zero_iff = thm "real_mult_self_eq_zero_iff";
 val real_sqrt_gt_zero = thm "real_sqrt_gt_zero";
 val real_sqrt_ge_zero = thm "real_sqrt_ge_zero";
 val sqrt_eqI = thm "sqrt_eqI";
@@ -2853,8 +2849,6 @@
 val real_sqrt_sum_squares_gt_zero2 = thm "real_sqrt_sum_squares_gt_zero2";
 val real_sqrt_sum_squares_gt_zero3 = thm "real_sqrt_sum_squares_gt_zero3";
 val real_sqrt_sum_squares_gt_zero3a = thm "real_sqrt_sum_squares_gt_zero3a";
-val real_sqrt_sum_squares_eq_cancel = thm "real_sqrt_sum_squares_eq_cancel";
-val real_sqrt_sum_squares_eq_cancel2 = thm "real_sqrt_sum_squares_eq_cancel2";
 val cos_x_y_ge_minus_one = thm "cos_x_y_ge_minus_one";
 val cos_x_y_ge_minus_one1a = thm "cos_x_y_ge_minus_one1a";
 val cos_x_y_le_one = thm "cos_x_y_le_one";