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