src/HOL/int_arith1.ML
changeset 23365 f31794033ae1
parent 23164 69e55066dbca
child 23400 a64b39e5809b
     1.1 --- a/src/HOL/int_arith1.ML	Wed Jun 13 03:28:21 2007 +0200
     1.2 +++ b/src/HOL/int_arith1.ML	Wed Jun 13 03:31:11 2007 +0200
     1.3 @@ -573,10 +573,11 @@
     1.4       @{thm mult_zero_left}, @{thm mult_zero_right}, @{thm mult_num1}, @{thm mult_1_right},
     1.5       @{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym,
     1.6       @{thm minus_add_distrib}, @{thm minus_minus}, @{thm mult_assoc},
     1.7 -     of_nat_0, of_nat_1, of_nat_Suc, of_nat_add, of_nat_mult,
     1.8 -     of_int_0, of_int_1, of_int_add, of_int_mult, int_eq_of_nat]
     1.9 +     @{thm of_nat_0}, @{thm of_nat_1}, @{thm of_nat_Suc}, @{thm of_nat_add},
    1.10 +     @{thm of_nat_mult}, @{thm of_int_0}, @{thm of_int_1}, @{thm of_int_add},
    1.11 +     @{thm of_int_mult}]
    1.12  
    1.13 -val nat_inj_thms = [zle_int RS iffD2, int_int_eq RS iffD2]
    1.14 +val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
    1.15  
    1.16  val Int_Numeral_Base_Simprocs = assoc_fold_simproc
    1.17    :: Int_Numeral_Simprocs.combine_numerals
    1.18 @@ -595,7 +596,6 @@
    1.19                        addsimprocs Int_Numeral_Base_Simprocs
    1.20                        addcongs [if_weak_cong]}) #>
    1.21    arith_inj_const ("Nat.of_nat", HOLogic.natT --> HOLogic.intT) #>
    1.22 -  arith_inj_const ("IntDef.int", HOLogic.natT --> HOLogic.intT) #>
    1.23    arith_discrete "IntDef.int"
    1.24  
    1.25  end;