diff -r bf523cac9a05 -r b5910e3dec4c src/HOL/Real/RealDef.thy --- a/src/HOL/Real/RealDef.thy Mon May 14 18:04:52 2007 +0200 +++ b/src/HOL/Real/RealDef.thy Mon May 14 18:48:24 2007 +0200 @@ -557,18 +557,6 @@ lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \ z*y) = (x\y)" by(simp add:mult_commute) -text{*FIXME: delete or at least combine the next two lemmas*} -lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)" -apply (drule OrderedGroup.equals_zero_I [THEN sym]) -apply (cut_tac x = y in real_le_square) -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: add_commute) -done - lemma real_add_order: "[| 0 < x; 0 < y |] ==> (0::real) < x + y" by (rule add_pos_pos) @@ -581,9 +569,6 @@ lemma real_inverse_gt_one: "[| (0::real) < x; x < 1 |] ==> 1 < inverse x" by (simp add: one_less_inverse_iff) -lemma real_mult_self_sum_ge_zero: "(0::real) \ x*x + y*y" -by (intro add_nonneg_nonneg zero_le_square) - subsection{*Embedding the Integers into the Reals*}