| changeset 44346 | 00dd3c4dabe0 |
| parent 44064 | 5bce8ff0d9ae |
| child 44350 | 63cddfbc5a09 |
--- 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