src/HOL/Real.thy
changeset 53076 47c9aff07725
parent 51956 a4d81cdebf8b
child 53374 a14d2a854c02
     1.1 --- a/src/HOL/Real.thy	Sun Aug 18 17:00:10 2013 +0200
     1.2 +++ b/src/HOL/Real.thy	Sun Aug 18 18:49:45 2013 +0200
     1.3 @@ -1559,13 +1559,13 @@
     1.4  
     1.5  text {* FIXME: declare this [simp] for all types, or not at all *}
     1.6  lemma realpow_two_sum_zero_iff [simp]:
     1.7 -     "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
     1.8 +     "(x\<^sup>2 + y\<^sup>2 = (0::real)) = (x = 0 & y = 0)"
     1.9  by (rule sum_power2_eq_zero_iff)
    1.10  
    1.11  lemma real_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))"
    1.12  by (rule_tac y = 0 in order_trans, auto)
    1.13  
    1.14 -lemma realpow_square_minus_le [simp]: "-(u ^ 2) \<le> (x::real) ^ 2"
    1.15 +lemma realpow_square_minus_le [simp]: "- u\<^sup>2 \<le> (x::real)\<^sup>2"
    1.16  by (auto simp add: power2_eq_square)
    1.17  
    1.18