1.1 --- a/src/HOL/RealDef.thy	Sat Aug 20 15:54:26 2011 -0700
     1.2 +++ b/src/HOL/RealDef.thy	Sat Aug 20 15:19:35 2011 -0700
     1.3 @@ -1601,12 +1601,6 @@
     1.4    shows "0 < n \<Longrightarrow> x ^ (n - 1) * x = x ^ n"
     1.5  by (simp add: power_commutes split add: nat_diff_split)
     1.6  
     1.7 -text {* TODO: no longer real-specific; rename and move elsewhere *}
     1.8 -lemma realpow_two_diff:
     1.9 -  fixes x :: "'a::comm_ring_1"
    1.10 -  shows "x^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"
    1.11 -by (simp add: algebra_simps)
    1.12 -
    1.13  text {* FIXME: declare this [simp] for all types, or not at all *}
    1.14  lemma real_two_squares_add_zero_iff [simp]:
    1.15    "(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)"

     2.1 --- a/src/HOL/Rings.thy	Sat Aug 20 15:54:26 2011 -0700
     2.2 +++ b/src/HOL/Rings.thy	Sat Aug 20 15:19:35 2011 -0700
     2.3 @@ -270,6 +270,10 @@
     2.4  subclass ring ..
     2.5  subclass comm_semiring_0_cancel ..
     2.6  
     2.7 +lemma square_diff_square_factored:
     2.8 +  "x * x - y * y = (x + y) * (x - y)"
     2.9 +  by (simp add: algebra_simps)
    2.10 +
    2.11  end
    2.12  
    2.13  class ring_1 = ring + zero_neq_one + monoid_mult