src/HOL/Number_Theory/MiscAlgebra.thy
changeset 60526 fad653acf58f
parent 57514 bdc2c6b40bf2
child 60527 eb431a5651fe
     1.1 --- a/src/HOL/Number_Theory/MiscAlgebra.thy	Fri Jun 19 21:33:03 2015 +0200
     1.2 +++ b/src/HOL/Number_Theory/MiscAlgebra.thy	Fri Jun 19 21:41:33 2015 +0200
     1.3 @@ -291,7 +291,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 from `x \<otimes> x = \<one>` have "\<dots> = \<zero>"
     1.8 +  also from \<open>x \<otimes> x = \<one>\<close> 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>"