# HG changeset patch
# User huffman
# Date 1313878775 25200
# Node ID 63cddfbc5a098a8ab5afc8b702c7340486ab140c
# Parent  f057535311c588459492bc5d4b0b6963375e4dc2
replace lemma realpow_two_diff with new lemma square_diff_square_factored

diff -r f057535311c5 -r 63cddfbc5a09 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Sat Aug 20 15:54:26 2011 -0700
+++ b/src/HOL/RealDef.thy	Sat Aug 20 15:19:35 2011 -0700
@@ -1601,12 +1601,6 @@
   shows "0 < n \<Longrightarrow> x ^ (n - 1) * x = x ^ n"
 by (simp add: power_commutes split add: nat_diff_split)
 
-text {* TODO: no longer real-specific; rename and move elsewhere *}
-lemma realpow_two_diff:
-  fixes x :: "'a::comm_ring_1"
-  shows "x^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"
-by (simp add: algebra_simps)
-
 text {* FIXME: declare this [simp] for all types, or not at all *}
 lemma real_two_squares_add_zero_iff [simp]:
   "(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)"
diff -r f057535311c5 -r 63cddfbc5a09 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Sat Aug 20 15:54:26 2011 -0700
+++ b/src/HOL/Rings.thy	Sat Aug 20 15:19:35 2011 -0700
@@ -270,6 +270,10 @@
 subclass ring ..
 subclass comm_semiring_0_cancel ..
 
+lemma square_diff_square_factored:
+  "x * x - y * y = (x + y) * (x - y)"
+  by (simp add: algebra_simps)
+
 end
 
 class ring_1 = ring + zero_neq_one + monoid_mult