src/HOL/Old_Number_Theory/WilsonRuss.thy

 (*  Title:      HOL/Old_Number_Theory/WilsonRuss.thy
     Author:     Thomas M. Rasmussen
     Copyright   2000  University of Cambridge
 *)
 
-section {* Wilson's Theorem according to Russinoff *}
+section \<open>Wilson's Theorem according to Russinoff\<close>
 
 theory WilsonRuss
 imports EulerFermat
 begin
 
-text {*
+text \<open>
   Wilson's Theorem following quite closely Russinoff's approach
   using Boyer-Moore (using finite sets instead of lists, though).
-*}
-
-subsection {* Definitions and lemmas *}
+\<close>
+
+subsection \<open>Definitions and lemmas\<close>
 
 definition inv :: "int => int => int"
   where "inv p a = (a^(nat (p - 2))) mod p"
 
 fun wset :: "int \<Rightarrow> int => int set" where

     (if 1 < a then
       let ws = wset (a - 1) p
       in (if a \<in> ws then ws else insert a (insert (inv p a) ws)) else {})"
 
 
-text {* \medskip @{term [source] inv} *}
+text \<open>\medskip @{term [source] inv}\<close>
 
 lemma inv_is_inv_aux: "1 < m ==> Suc (nat (m - 2)) = nat (m - 1)"
   by (subst int_int_eq [symmetric]) auto
 
 lemma inv_is_inv:

          apply (erule_tac [4] Little_Fermat)
          apply (rule_tac [4] zdvd_not_zless, simp_all)
   done
 
 
-text {* \medskip @{term wset} *}
+text \<open>\medskip @{term wset}\<close>
 
 declare wset.simps [simp del]
 
 lemma wset_induct:
   assumes "!!a p. P {} a p"

   apply (induct a p rule: wset_induct)
    prefer 2
    apply (subst wset.simps)
    apply (auto, unfold Let_def, auto)
   apply (subst setprod.insert)
-    apply (tactic {* stac @{context} @{thm setprod.insert} 3 *})
+    apply (tactic \<open>stac @{context} @{thm setprod.insert} 3\<close>)
       apply (subgoal_tac [5]
         "zcong (a * inv p a * (\<Prod>x\<in>wset (a - 1) p. x)) (1 * 1) p")
        prefer 5
        apply (simp add: mult.assoc)
       apply (rule_tac [5] zcong_zmult)

         apply (simp (no_asm_simp))
         apply (erule wset_less, auto)
   done
 
 
-subsection {* Wilson *}
+subsection \<open>Wilson\<close>
 
 lemma prime_g_5: "zprime p \<Longrightarrow> p \<noteq> 2 \<Longrightarrow> p \<noteq> 3 ==> 5 \<le> p"
   apply (unfold zprime_def dvd_def)
   apply (case_tac "p = 4", auto)
    apply (rule notE)