src/HOL/Divides.thy
changeset 46026 83caa4f4bd56
parent 45607 16b4f5774621
child 46551 866bce5442a3
     1.1 --- a/src/HOL/Divides.thy	Wed Dec 28 22:08:44 2011 +0100
     1.2 +++ b/src/HOL/Divides.thy	Thu Dec 29 10:47:54 2011 +0100
     1.3 @@ -2418,7 +2418,7 @@
     1.4  
     1.5  lemma one_div_nat_number_of [simp]:
     1.6       "Suc 0 div number_of v' = nat (1 div number_of v')" 
     1.7 -by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
     1.8 +  by (simp del: semiring_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric] semiring_numeral_1_eq_1 [symmetric]) 
     1.9  
    1.10  lemma mod_nat_number_of [simp]:
    1.11       "(number_of v :: nat)  mod  number_of v' =  
    1.12 @@ -2432,7 +2432,7 @@
    1.13       "Suc 0 mod number_of v' =  
    1.14          (if neg (number_of v' :: int) then Suc 0
    1.15           else nat (1 mod number_of v'))"
    1.16 -by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
    1.17 +by (simp del: semiring_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric] semiring_numeral_1_eq_1 [symmetric]) 
    1.18  
    1.19  lemmas dvd_eq_mod_eq_0_number_of [simp] =
    1.20    dvd_eq_mod_eq_0 [of "number_of x" "number_of y"] for x y