diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/Old_Number_Theory/WilsonBij.thy
--- a/src/HOL/Old_Number_Theory/WilsonBij.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonBij.thy	Thu May 26 17:51:22 2016 +0200
@@ -47,7 +47,7 @@
 
 lemma inv_not_0:
   "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> 0"
-  -- \<open>same as @{text WilsonRuss}\<close>
+  \<comment> \<open>same as \<open>WilsonRuss\<close>\<close>
   apply safe
   apply (cut_tac a = a and p = p in inv_is_inv)
      apply (unfold zcong_def)
@@ -56,7 +56,7 @@
 
 lemma inv_not_1:
   "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> 1"
-  -- \<open>same as @{text WilsonRuss}\<close>
+  \<comment> \<open>same as \<open>WilsonRuss\<close>\<close>
   apply safe
   apply (cut_tac a = a and p = p in inv_is_inv)
      prefer 4
@@ -67,7 +67,7 @@
   done
 
 lemma aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
-  -- \<open>same as @{text WilsonRuss}\<close>
+  \<comment> \<open>same as \<open>WilsonRuss\<close>\<close>
   apply (unfold zcong_def)
   apply (simp add: diff_diff_eq diff_diff_eq2 right_diff_distrib)
   apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
@@ -81,7 +81,7 @@
 
 lemma inv_not_p_minus_1:
   "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> p - 1"
-  -- \<open>same as @{text WilsonRuss}\<close>
+  \<comment> \<open>same as \<open>WilsonRuss\<close>\<close>
   apply safe
   apply (cut_tac a = a and p = p in inv_is_inv)
      apply auto
@@ -93,7 +93,7 @@
 
 text \<open>
   Below is slightly different as we don't expand @{term [source] inv}
-  but use ``@{text correct}'' theorems.
+  but use ``\<open>correct\<close>'' theorems.
 \<close>
 
 lemma inv_g_1: "zprime p ==> 1 < a ==> a < p - 1 ==> 1 < inv p a"
@@ -111,7 +111,7 @@
 
 lemma inv_less_p_minus_1:
   "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a < p - 1"
-  -- \<open>ditto\<close>
+  \<comment> \<open>ditto\<close>
   apply (subst order_less_le)
   apply (simp add: inv_not_p_minus_1 inv_less)
   done