src/HOL/NumberTheory/WilsonRuss.thy
changeset 13788 fd03c4ab89d4
parent 13524 604d0f3622d6
child 13833 f8dcb1d9ea68
     1.1 --- a/src/HOL/NumberTheory/WilsonRuss.thy	Mon Jan 27 10:39:31 2003 +0100
     1.2 +++ b/src/HOL/NumberTheory/WilsonRuss.thy	Tue Jan 28 07:39:29 2003 +0100
     1.3 @@ -124,7 +124,7 @@
     1.4         apply (rule_tac [5] inv_not_1)
     1.5           apply auto
     1.6    apply (unfold inv_def zprime_def)
     1.7 -  apply (simp add: pos_mod_sign)
     1.8 +  apply (simp)
     1.9    done
    1.10  
    1.11  lemma inv_less_p_minus_1:
    1.12 @@ -134,7 +134,7 @@
    1.13     apply (simp add: inv_not_p_minus_1)
    1.14    apply auto
    1.15    apply (unfold inv_def zprime_def)
    1.16 -  apply (simp add: pos_mod_bound)
    1.17 +  apply (simp)
    1.18    done
    1.19  
    1.20  lemma inv_inv_aux: "5 \<le> p ==>
    1.21 @@ -170,7 +170,7 @@
    1.22           apply (rule_tac [4] zcong_zpower_zmult)
    1.23           apply (erule_tac [4] Little_Fermat)
    1.24           apply (rule_tac [4] zdvd_not_zless)
    1.25 -          apply (simp_all add: pos_mod_bound pos_mod_sign)
    1.26 +          apply (simp_all)
    1.27    done
    1.28  
    1.29