src/HOL/Import/HOL/arithmetic.imp
changeset 31790 05c92381363c
parent 30925 c38cbc0ac8d1
child 33657 a4179bf442d1
     1.1 --- a/src/HOL/Import/HOL/arithmetic.imp	Tue Jun 23 21:07:39 2009 +0200
     1.2 +++ b/src/HOL/Import/HOL/arithmetic.imp	Wed Jun 24 09:41:14 2009 +0200
     1.3 @@ -43,7 +43,7 @@
     1.4    "TWO" > "HOL4Base.arithmetic.TWO"
     1.5    "TIMES2" > "NatSimprocs.nat_mult_2"
     1.6    "SUC_SUB1" > "HOL4Base.arithmetic.SUC_SUB1"
     1.7 -  "SUC_ONE_ADD" > "Nat_Numeral.Suc_eq_add_numeral_1_left"
     1.8 +  "SUC_ONE_ADD" > "Nat_Numeral.Suc_eq_plus1_left"
     1.9    "SUC_NOT" > "Nat.nat.simps_2"
    1.10    "SUC_ELIM_THM" > "HOL4Base.arithmetic.SUC_ELIM_THM"
    1.11    "SUC_ADD_SYM" > "HOL4Base.arithmetic.SUC_ADD_SYM"
    1.12 @@ -265,7 +265,7 @@
    1.13    "ADD_CLAUSES" > "HOL4Base.arithmetic.ADD_CLAUSES"
    1.14    "ADD_ASSOC" > "Finite_Set.AC_add.f.AC_1"
    1.15    "ADD_0" > "Finite_Set.AC_add.f_e.ident"
    1.16 -  "ADD1" > "Presburger.Suc_plus1"
    1.17 +  "ADD1" > "Nat_Numeral.Suc_eq_plus1"
    1.18    "ADD" > "HOL4Compat.ADD"
    1.19  
    1.20  end