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