src/HOL/Old_Number_Theory/WilsonRuss.thy
changeset 61382 efac889fccbc
parent 59498 50b60f501b05
child 61649 268d88ec9087
     1.1 --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Sat Oct 10 16:21:34 2015 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Sat Oct 10 16:26:23 2015 +0200
     1.3 @@ -3,18 +3,18 @@
     1.4      Copyright   2000  University of Cambridge
     1.5  *)
     1.6  
     1.7 -section {* Wilson's Theorem according to Russinoff *}
     1.8 +section \<open>Wilson's Theorem according to Russinoff\<close>
     1.9  
    1.10  theory WilsonRuss
    1.11  imports EulerFermat
    1.12  begin
    1.13  
    1.14 -text {*
    1.15 +text \<open>
    1.16    Wilson's Theorem following quite closely Russinoff's approach
    1.17    using Boyer-Moore (using finite sets instead of lists, though).
    1.18 -*}
    1.19 +\<close>
    1.20  
    1.21 -subsection {* Definitions and lemmas *}
    1.22 +subsection \<open>Definitions and lemmas\<close>
    1.23  
    1.24  definition inv :: "int => int => int"
    1.25    where "inv p a = (a^(nat (p - 2))) mod p"
    1.26 @@ -26,7 +26,7 @@
    1.27        in (if a \<in> ws then ws else insert a (insert (inv p a) ws)) else {})"
    1.28  
    1.29  
    1.30 -text {* \medskip @{term [source] inv} *}
    1.31 +text \<open>\medskip @{term [source] inv}\<close>
    1.32  
    1.33  lemma inv_is_inv_aux: "1 < m ==> Suc (nat (m - 2)) = nat (m - 1)"
    1.34    by (subst int_int_eq [symmetric]) auto
    1.35 @@ -149,7 +149,7 @@
    1.36    done
    1.37  
    1.38  
    1.39 -text {* \medskip @{term wset} *}
    1.40 +text \<open>\medskip @{term wset}\<close>
    1.41  
    1.42  declare wset.simps [simp del]
    1.43  
    1.44 @@ -252,7 +252,7 @@
    1.45     apply (subst wset.simps)
    1.46     apply (auto, unfold Let_def, auto)
    1.47    apply (subst setprod.insert)
    1.48 -    apply (tactic {* stac @{context} @{thm setprod.insert} 3 *})
    1.49 +    apply (tactic \<open>stac @{context} @{thm setprod.insert} 3\<close>)
    1.50        apply (subgoal_tac [5]
    1.51          "zcong (a * inv p a * (\<Prod>x\<in>wset (a - 1) p. x)) (1 * 1) p")
    1.52         prefer 5
    1.53 @@ -281,7 +281,7 @@
    1.54    done
    1.55  
    1.56  
    1.57 -subsection {* Wilson *}
    1.58 +subsection \<open>Wilson\<close>
    1.59  
    1.60  lemma prime_g_5: "zprime p \<Longrightarrow> p \<noteq> 2 \<Longrightarrow> p \<noteq> 3 ==> 5 \<le> p"
    1.61    apply (unfold zprime_def dvd_def)