src/HOL/Old_Number_Theory/Residues.thy
changeset 41541 1fa4725c4656
parent 38159 e9b4835a54ee
child 53077 a1b3784f8129
     1.1 --- a/src/HOL/Old_Number_Theory/Residues.thy	Thu Jan 13 21:50:13 2011 +0100
     1.2 +++ b/src/HOL/Old_Number_Theory/Residues.thy	Thu Jan 13 23:50:16 2011 +0100
     1.3 @@ -51,10 +51,10 @@
     1.4                       mod_mult_eq [of x y m])
     1.5  
     1.6  lemma StandardRes_lbound: "0 < p ==> 0 \<le> StandardRes p x"
     1.7 -  by (auto simp add: StandardRes_def pos_mod_sign)
     1.8 +  by (auto simp add: StandardRes_def)
     1.9  
    1.10  lemma StandardRes_ubound: "0 < p ==> StandardRes p x < p"
    1.11 -  by (auto simp add: StandardRes_def pos_mod_bound)
    1.12 +  by (auto simp add: StandardRes_def)
    1.13  
    1.14  lemma StandardRes_eq_zcong: 
    1.15     "(StandardRes m x = 0) = ([x = 0](mod m))"
    1.16 @@ -71,8 +71,7 @@
    1.17  
    1.18  lemma StandardRes_SRStar_prop1: "2 < p ==> (StandardRes p x \<in> SRStar p) 
    1.19       = (~[x = 0] (mod p))"
    1.20 -  apply (auto simp add: StandardRes_prop3 StandardRes_def
    1.21 -                        SRStar_def pos_mod_bound)
    1.22 +  apply (auto simp add: StandardRes_prop3 StandardRes_def SRStar_def)
    1.23    apply (subgoal_tac "0 < p")
    1.24    apply (drule_tac a = x in pos_mod_sign, arith, simp)
    1.25    done