diff -r 0836569a8ffc -r 13e9c402308b src/HOL/NumberTheory/EulerFermat.thy
--- a/src/HOL/NumberTheory/EulerFermat.thy	Fri Jul 01 14:55:05 2005 +0200
+++ b/src/HOL/NumberTheory/EulerFermat.thy	Fri Jul 01 17:41:10 2005 +0200
@@ -316,7 +316,7 @@
   done
 
 lemma Bnor_prime [rule_format (no_asm)]:
-  "p \<in> zprime ==>
+  "zprime p ==>
     a < p --> (\<forall>b. 0 < b \<and> b \<le> a --> zgcd (b, p) = 1)
     --> card (BnorRset (a, p)) = nat a"
   apply (auto simp add: zless_zprime_imp_zrelprime)
@@ -330,14 +330,14 @@
   apply (frule Bnor_fin)
   done
 
-lemma phi_prime: "p \<in> zprime ==> phi p = nat (p - 1)"
+lemma phi_prime: "zprime p ==> phi p = nat (p - 1)"
   apply (unfold phi_def norRRset_def)
   apply (rule Bnor_prime, auto)
   apply (erule zless_zprime_imp_zrelprime, simp_all)
   done
 
 theorem Little_Fermat:
-    "p \<in> zprime ==> \<not> p dvd x ==> [x^(nat (p - 1)) = 1] (mod p)"
+    "zprime p ==> \<not> p dvd x ==> [x^(nat (p - 1)) = 1] (mod p)"
   apply (subst phi_prime [symmetric])
    apply (rule_tac [2] Euler_Fermat)
     apply (erule_tac [3] zprime_imp_zrelprime)