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)