src/HOL/Old_Number_Theory/EulerFermat.thy
 changeset 63167 0909deb8059b parent 61945 1135b8de26c3 child 64272 f76b6dda2e56
```     1.1 --- a/src/HOL/Old_Number_Theory/EulerFermat.thy	Thu May 26 16:57:14 2016 +0200
1.2 +++ b/src/HOL/Old_Number_Theory/EulerFermat.thy	Thu May 26 17:51:22 2016 +0200
1.3 @@ -54,11 +54,11 @@
1.4    where "zcongm m = (\<lambda>a b. zcong a b m)"
1.5
1.6  lemma abs_eq_1_iff [iff]: "(\<bar>z\<bar> = (1::int)) = (z = 1 \<or> z = -1)"
1.7 -  -- \<open>LCP: not sure why this lemma is needed now\<close>
1.8 +  \<comment> \<open>LCP: not sure why this lemma is needed now\<close>
1.9    by (auto simp add: abs_if)
1.10
1.11
1.12 -text \<open>\medskip @{text norRRset}\<close>
1.13 +text \<open>\medskip \<open>norRRset\<close>\<close>
1.14
1.15  declare BnorRset.simps [simp del]
1.16
1.17 @@ -249,7 +249,7 @@
1.18        \<Prod>(BnorRset a m) * x^card (BnorRset a m)"
1.19    apply (induct a m rule: BnorRset_induct)
1.20     prefer 2
1.21 -   apply (simplesubst BnorRset.simps)  --\<open>multiple redexes\<close>
1.22 +   apply (simplesubst BnorRset.simps)  \<comment>\<open>multiple redexes\<close>
1.23     apply (unfold Let_def, auto)
1.24    apply (simp add: Bnor_fin Bnor_mem_zle_swap)
1.25    apply (subst setprod.insert)
```