src/HOL/Rings.thy
changeset 36970 fb3fdb4b585e
parent 36821 9207505d1ee5
child 36977 71c8973a604b
     1.1 --- a/src/HOL/Rings.thy	Mon May 17 08:40:17 2010 -0700
     1.2 +++ b/src/HOL/Rings.thy	Mon May 17 08:45:46 2010 -0700
     1.3 @@ -349,7 +349,7 @@
     1.4  class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
     1.5  begin
     1.6  
     1.7 -lemma square_eq_1_iff [simp]:
     1.8 +lemma square_eq_1_iff:
     1.9    "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"
    1.10  proof -
    1.11    have "(x - 1) * (x + 1) = x * x - 1"