--- a/src/HOL/Number_Theory/Residues.thy Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Number_Theory/Residues.thy Thu May 26 17:51:22 2016 +0200
@@ -124,7 +124,7 @@
by (subst res_units_eq) auto
text \<open>
- The function @{text "a \<mapsto> a mod m"} maps the integers to the
+ The function \<open>a \<mapsto> a mod m\<close> maps the integers to the
residue classes. The following lemmas show that this mapping
respects addition and multiplication on the integers.
\<close>
@@ -327,7 +327,7 @@
*)
-text \<open>Outside the locale, we can relax the restriction @{text "m > 1"}.\<close>
+text \<open>Outside the locale, we can relax the restriction \<open>m > 1\<close>.\<close>
lemma euler_theorem:
assumes "m \<ge> 0"
and "gcd a m = 1"