src/HOL/Old_Number_Theory/EulerFermat.thy
changeset 61382 efac889fccbc
parent 58889 5b7a9633cfa8
child 61945 1135b8de26c3
     1.1 --- a/src/HOL/Old_Number_Theory/EulerFermat.thy	Sat Oct 10 16:21:34 2015 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/EulerFermat.thy	Sat Oct 10 16:26:23 2015 +0200
     1.3 @@ -3,20 +3,20 @@
     1.4      Copyright   2000  University of Cambridge
     1.5  *)
     1.6  
     1.7 -section {* Fermat's Little Theorem extended to Euler's Totient function *}
     1.8 +section \<open>Fermat's Little Theorem extended to Euler's Totient function\<close>
     1.9  
    1.10  theory EulerFermat
    1.11  imports BijectionRel IntFact
    1.12  begin
    1.13  
    1.14 -text {*
    1.15 +text \<open>
    1.16    Fermat's Little Theorem extended to Euler's Totient function. More
    1.17    abstract approach than Boyer-Moore (which seems necessary to achieve
    1.18    the extended version).
    1.19 -*}
    1.20 +\<close>
    1.21  
    1.22  
    1.23 -subsection {* Definitions and lemmas *}
    1.24 +subsection \<open>Definitions and lemmas\<close>
    1.25  
    1.26  inductive_set RsetR :: "int => int set set" for m :: int
    1.27  where
    1.28 @@ -54,11 +54,11 @@
    1.29    where "zcongm m = (\<lambda>a b. zcong a b m)"
    1.30  
    1.31  lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)"
    1.32 -  -- {* LCP: not sure why this lemma is needed now *}
    1.33 +  -- \<open>LCP: not sure why this lemma is needed now\<close>
    1.34    by (auto simp add: abs_if)
    1.35  
    1.36  
    1.37 -text {* \medskip @{text norRRset} *}
    1.38 +text \<open>\medskip @{text norRRset}\<close>
    1.39  
    1.40  declare BnorRset.simps [simp del]
    1.41  
    1.42 @@ -146,7 +146,7 @@
    1.43    done
    1.44  
    1.45  
    1.46 -text {* \medskip @{term noXRRset} *}
    1.47 +text \<open>\medskip @{term noXRRset}\<close>
    1.48  
    1.49  lemma RRset_gcd [rule_format]:
    1.50      "is_RRset A m ==> a \<in> A --> zgcd a m = 1"
    1.51 @@ -249,7 +249,7 @@
    1.52        \<Prod>(BnorRset a m) * x^card (BnorRset a m)"
    1.53    apply (induct a m rule: BnorRset_induct)
    1.54     prefer 2
    1.55 -   apply (simplesubst BnorRset.simps)  --{*multiple redexes*}
    1.56 +   apply (simplesubst BnorRset.simps)  --\<open>multiple redexes\<close>
    1.57     apply (unfold Let_def, auto)
    1.58    apply (simp add: Bnor_fin Bnor_mem_zle_swap)
    1.59    apply (subst setprod.insert)
    1.60 @@ -259,7 +259,7 @@
    1.61    done
    1.62  
    1.63  
    1.64 -subsection {* Fermat *}
    1.65 +subsection \<open>Fermat\<close>
    1.66  
    1.67  lemma bijzcong_zcong_prod:
    1.68      "(A, B) \<in> bijR (zcongm m) ==> [\<Prod>A = \<Prod>B] (mod m)"