src/HOL/Number_Theory/Residues.thy
changeset 63167 0909deb8059b
parent 62348 9a5f43dac883
child 63417 c184ec919c70
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Thu May 26 16:57:14 2016 +0200
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Thu May 26 17:51:22 2016 +0200
     1.3 @@ -124,7 +124,7 @@
     1.4    by (subst res_units_eq) auto
     1.5  
     1.6  text \<open>
     1.7 -  The function @{text "a \<mapsto> a mod m"} maps the integers to the
     1.8 +  The function \<open>a \<mapsto> a mod m\<close> maps the integers to the
     1.9    residue classes. The following lemmas show that this mapping
    1.10    respects addition and multiplication on the integers.
    1.11  \<close>
    1.12 @@ -327,7 +327,7 @@
    1.13  
    1.14  *)
    1.15  
    1.16 -text \<open>Outside the locale, we can relax the restriction @{text "m > 1"}.\<close>
    1.17 +text \<open>Outside the locale, we can relax the restriction \<open>m > 1\<close>.\<close>
    1.18  lemma euler_theorem:
    1.19    assumes "m \<ge> 0"
    1.20      and "gcd a m = 1"