1.1 --- a/src/HOL/NumberTheory/WilsonBij.thy	Fri Oct 05 23:58:52 2001 +0200
     1.2 +++ b/src/HOL/NumberTheory/WilsonBij.thy	Sat Oct 06 00:02:46 2001 +0200
     1.3 @@ -133,15 +133,15 @@
     1.4    apply auto
     1.5    done
     1.6  
     1.7 -lemma aux3: "x \<le> p - # 2 ==> x < (p::int)"
     1.8 +lemma aux3: "x \<le> p - 2 ==> x < (p::int)"
     1.9    apply auto
    1.10    done
    1.11  
    1.12 -lemma aux4: "x \<le> p - # 2 ==> x < (p::int)-Numeral1"
    1.13 +lemma aux4: "x \<le> p - 2 ==> x < (p::int)-Numeral1"
    1.14    apply auto
    1.15    done
    1.16  
    1.17 -lemma inv_inj: "p \<in> zprime ==> inj_on (inv p) (d22set (p - # 2))"
    1.18 +lemma inv_inj: "p \<in> zprime ==> inj_on (inv p) (d22set (p - 2))"
    1.19    apply (unfold inj_on_def)
    1.20    apply auto
    1.21    apply (rule zcong_zless_imp_eq)
    1.22 @@ -160,7 +160,7 @@
    1.23    done
    1.24  
    1.25  lemma inv_d22set_d22set:
    1.26 -    "p \<in> zprime ==> inv p ` d22set (p - # 2) = d22set (p - # 2)"
    1.27 +    "p \<in> zprime ==> inv p ` d22set (p - 2) = d22set (p - 2)"
    1.28    apply (rule endo_inj_surj)
    1.29      apply (rule d22set_fin)
    1.30     apply (erule_tac [2] inv_inj)
    1.31 @@ -173,9 +173,9 @@
    1.32    done
    1.33  
    1.34  lemma d22set_d22set_bij:
    1.35 -    "p \<in> zprime ==> (d22set (p - # 2), d22set (p - # 2)) \<in> bijR (reciR p)"
    1.36 +    "p \<in> zprime ==> (d22set (p - 2), d22set (p - 2)) \<in> bijR (reciR p)"
    1.37    apply (unfold reciR_def)
    1.38 -  apply (rule_tac s = "(d22set (p - # 2), inv p ` d22set (p - # 2))" in subst)
    1.39 +  apply (rule_tac s = "(d22set (p - 2), inv p ` d22set (p - 2))" in subst)
    1.40     apply (simp add: inv_d22set_d22set)
    1.41    apply (rule inj_func_bijR)
    1.42      apply (rule_tac [3] d22set_fin)
    1.43 @@ -187,7 +187,7 @@
    1.44           apply (auto intro: d22set_g_1 d22set_le aux2 aux3 aux4)
    1.45    done
    1.46  
    1.47 -lemma reciP_bijP: "p \<in> zprime ==> bijP (reciR p) (d22set (p - # 2))"
    1.48 +lemma reciP_bijP: "p \<in> zprime ==> bijP (reciR p) (d22set (p - 2))"
    1.49    apply (unfold reciR_def bijP_def)
    1.50    apply auto
    1.51    apply (rule d22set_mem)
    1.52 @@ -217,7 +217,7 @@
    1.53    apply auto
    1.54    done
    1.55  
    1.56 -lemma bijER_d22set: "p \<in> zprime ==> d22set (p - # 2) \<in> bijER (reciR p)"
    1.57 +lemma bijER_d22set: "p \<in> zprime ==> d22set (p - 2) \<in> bijER (reciR p)"
    1.58    apply (rule bijR_bijER)
    1.59       apply (erule d22set_d22set_bij)
    1.60      apply (erule reciP_bijP)
    1.61 @@ -245,12 +245,12 @@
    1.62     apply auto
    1.63    done
    1.64  
    1.65 -theorem Wilson_Bij: "p \<in> zprime ==> [zfact (p - Numeral1) = # -1] (mod p)"
    1.66 -  apply (subgoal_tac "zcong ((p - Numeral1) * zfact (p - # 2)) (# -1 * Numeral1) p")
    1.67 +theorem Wilson_Bij: "p \<in> zprime ==> [zfact (p - Numeral1) = -1] (mod p)"
    1.68 +  apply (subgoal_tac "zcong ((p - Numeral1) * zfact (p - 2)) (-1 * Numeral1) p")
    1.69     apply (rule_tac [2] zcong_zmult)
    1.70      apply (simp add: zprime_def)
    1.71      apply (subst zfact.simps)
    1.72 -    apply (rule_tac t = "p - Numeral1 - Numeral1" and s = "p - # 2" in subst)
    1.73 +    apply (rule_tac t = "p - Numeral1 - Numeral1" and s = "p - 2" in subst)
    1.74       apply auto
    1.75     apply (simp add: zcong_def)
    1.76    apply (subst d22set_prod_zfact [symmetric])