src/HOL/Number_Theory/Residues.thy
 changeset 60526 fad653acf58f parent 59730 b7c394c7a619 child 60527 eb431a5651fe
```     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Fri Jun 19 21:33:03 2015 +0200
1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Fri Jun 19 21:41:33 2015 +0200
1.3 @@ -5,7 +5,7 @@
1.4  Euler's theorem and Wilson's theorem.
1.5  *)
1.6
1.7 -section {* Residue rings *}
1.8 +section \<open>Residue rings\<close>
1.9
1.10  theory Residues
1.11  imports UniqueFactorization MiscAlgebra
1.12 @@ -248,7 +248,7 @@
1.13  *)
1.14
1.15
1.16 -subsection{* Euler's theorem *}
1.17 +subsection\<open>Euler's theorem\<close>
1.18
1.19  (* the definition of the phi function *)
1.20
1.21 @@ -276,9 +276,9 @@
1.22        apply (rule cop)
1.23        using * apply auto
1.24        done
1.25 -    with `x dvd p` `1 < x` have "False" by auto }
1.26 +    with \<open>x dvd p\<close> \<open>1 < x\<close> have "False" by auto }
1.27    then show ?thesis
1.28 -    using `2 \<le> p`
1.29 +    using \<open>2 \<le> p\<close>