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>
    1.30      by (simp add: prime_def)
    1.31         (metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0
    1.32                not_numeral_le_zero one_dvd)
    1.33 @@ -374,7 +374,7 @@
    1.34  by (metis int_1 of_nat_power transfer_int_nat_cong zdvd_int)
    1.35  
    1.36  
    1.37 -subsection {* Wilson's theorem *}
    1.38 +subsection \<open>Wilson's theorem\<close>
    1.39  
    1.40  lemma (in field) inv_pair_lemma: "x : Units R \<Longrightarrow> y : Units R \<Longrightarrow>
    1.41      {x, inv x} ~= {y, inv y} \<Longrightarrow> {x, inv x} Int {y, inv y} = {}"