src/HOL/Real/RealPow.thy
changeset 15085 5693a977a767
parent 15003 6145dd7538d7
child 15131 c69542757a4d
     1.1 --- a/src/HOL/Real/RealPow.thy	Thu Jul 29 16:14:06 2004 +0200
     1.2 +++ b/src/HOL/Real/RealPow.thy	Thu Jul 29 16:14:42 2004 +0200
     1.3 @@ -140,7 +140,9 @@
     1.4  
     1.5  text{*Used several times in Hyperreal/Transcendental.ML*}
     1.6  lemma real_sum_squares_cancel_a: "x * x = -(y * y) ==> x = (0::real) & y=0"
     1.7 -  by (auto intro: real_sum_squares_cancel)
     1.8 +  apply (auto dest: real_sum_squares_cancel simp add: real_add_eq_0_iff [symmetric])
     1.9 +  apply (auto dest: real_sum_squares_cancel simp add: add_commute)
    1.10 +  done
    1.11  
    1.12  lemma real_squared_diff_one_factored: "x*x - (1::real) = (x + 1)*(x - 1)"
    1.13  by (auto simp add: left_distrib right_distrib real_diff_def)