# HG changeset patch
# User huffman
# Date 1313860127 25200
# Node ID 00dd3c4dabe083a91a8475320f87db223dc5ed45
# Parent  881c324470a24010b8563ca871dd2f229fcb4608
rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy

diff -r 881c324470a2 -r 00dd3c4dabe0 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Sat Aug 20 09:59:28 2011 -0700
+++ b/src/HOL/RealDef.thy	Sat Aug 20 10:08:47 2011 -0700
@@ -1630,12 +1630,6 @@
   "(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)"
 by (rule sum_squares_eq_zero_iff)
 
-text {* TODO: no longer real-specific; rename and move elsewhere *}
-lemma real_squared_diff_one_factored:
-  fixes x :: "'a::ring_1"
-  shows "x * x - 1 = (x + 1) * (x - 1)"
-by (simp add: algebra_simps)
-
 text {* FIXME: declare this [simp] for all types, or not at all *}
 lemma realpow_two_sum_zero_iff [simp]:
      "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
diff -r 881c324470a2 -r 00dd3c4dabe0 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Sat Aug 20 09:59:28 2011 -0700
+++ b/src/HOL/Rings.thy	Sat Aug 20 10:08:47 2011 -0700
@@ -277,6 +277,10 @@
 
 subclass semiring_1_cancel ..
 
+lemma square_diff_one_factored:
+  "x * x - 1 = (x + 1) * (x - 1)"
+  by (simp add: algebra_simps)
+
 end
 
 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult