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)"
```