src/HOL/Number_Theory/MiscAlgebra.thy
changeset 53374 a14d2a854c02
parent 44890 22f665a2e91c
child 55322 3bf50e3cd727
     1.1 --- a/src/HOL/Number_Theory/MiscAlgebra.thy	Tue Sep 03 00:51:08 2013 +0200
     1.2 +++ b/src/HOL/Number_Theory/MiscAlgebra.thy	Tue Sep 03 01:12:40 2013 +0200
     1.3 @@ -298,7 +298,7 @@
     1.4  proof -
     1.5    have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>"
     1.6      by (simp add: ring_simprules)
     1.7 -  also with `x \<otimes> x = \<one>` have "\<dots> = \<zero>"
     1.8 +  also from `x \<otimes> x = \<one>` have "\<dots> = \<zero>"
     1.9      by (simp add: ring_simprules)
    1.10    finally have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = \<zero>" .
    1.11    then have "(x \<oplus> \<one>) = \<zero> | (x \<oplus> \<ominus> \<one>) = \<zero>"