diff -r 278b65d9339c -r fad653acf58f src/HOL/Number_Theory/MiscAlgebra.thy
--- a/src/HOL/Number_Theory/MiscAlgebra.thy Fri Jun 19 21:33:03 2015 +0200
+++ b/src/HOL/Number_Theory/MiscAlgebra.thy Fri Jun 19 21:41:33 2015 +0200
@@ -291,7 +291,7 @@
proof -
have "(x \ \) \ (x \ \ \) = x \ x \ \ \"
by (simp add: ring_simprules)
- also from `x \ x = \` have "\ = \"
+ also from \x \ x = \\ have "\ = \"
by (simp add: ring_simprules)
finally have "(x \ \) \ (x \ \ \) = \" .
then have "(x \ \) = \ | (x \ \ \) = \"