src/HOL/Rings.thy

--- a/src/HOL/Rings.thy	Mon May 17 08:40:17 2010 -0700
+++ b/src/HOL/Rings.thy	Mon May 17 08:45:46 2010 -0700
@@ -349,7 +349,7 @@
 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
 begin
 
-lemma square_eq_1_iff [simp]:
+lemma square_eq_1_iff:
   "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"
 proof -
   have "(x - 1) * (x + 1) = x * x - 1"