adjusted to constant and theorem renames
authorhaftmann
Mon Jan 21 08:43:30 2008 +0100 (2008-01-21)
changeset 2593083e3dd60affe
parent 25929 6bfef23e26be
child 25931 b1d1ab3e5a2e
adjusted to constant and theorem renames
src/HOL/Import/HOL/arithmetic.imp
src/HOL/Import/HOL/real.imp
src/HOL/Import/HOL/realax.imp
src/HOL/Import/HOLLight/hollight.imp
     1.1 --- a/src/HOL/Import/HOL/arithmetic.imp	Mon Jan 21 08:43:29 2008 +0100
     1.2 +++ b/src/HOL/Import/HOL/arithmetic.imp	Mon Jan 21 08:43:30 2008 +0100
     1.3 @@ -108,7 +108,7 @@
     1.4    "NOT_GREATER" > "Nat.le_def"
     1.5    "NOT_EXP_0" > "HOL4Base.arithmetic.NOT_EXP_0"
     1.6    "NORM_0" > "HOL4Base.arithmetic.NORM_0"
     1.7 -  "MULT_SYM" > "IntDef.zmult_ac_2"
     1.8 +  "MULT_SYM" > "Int.zmult_ac_2"
     1.9    "MULT_SUC_EQ" > "HOL4Base.arithmetic.MULT_SUC_EQ"
    1.10    "MULT_SUC" > "Nat.mult_Suc_right"
    1.11    "MULT_RIGHT_1" > "Finite_Set.AC_mult.f_e.ident"
    1.12 @@ -120,9 +120,9 @@
    1.13    "MULT_EQ_1" > "HOL4Base.arithmetic.MULT_EQ_1"
    1.14    "MULT_EQ_0" > "Nat.mult_is_0"
    1.15    "MULT_DIV" > "Divides.div_mult_self_is_m"
    1.16 -  "MULT_COMM" > "IntDef.zmult_ac_2"
    1.17 +  "MULT_COMM" > "Int.zmult_ac_2"
    1.18    "MULT_CLAUSES" > "HOL4Base.arithmetic.MULT_CLAUSES"
    1.19 -  "MULT_ASSOC" > "IntDef.zmult_ac_1"
    1.20 +  "MULT_ASSOC" > "Int.zmult_ac_1"
    1.21    "MULT_0" > "Nat.mult_0_right"
    1.22    "MULT" > "HOL4Compat.MULT"
    1.23    "MOD_UNIQUE" > "HOL4Base.arithmetic.MOD_UNIQUE"
     2.1 --- a/src/HOL/Import/HOL/real.imp	Mon Jan 21 08:43:29 2008 +0100
     2.2 +++ b/src/HOL/Import/HOL/real.imp	Mon Jan 21 08:43:30 2008 +0100
     2.3 @@ -129,7 +129,7 @@
     2.4    "REAL_NEG_ADD" > "OrderedGroup.minus_add_distrib"
     2.5    "REAL_NEG_0" > "OrderedGroup.minus_zero"
     2.6    "REAL_NEGNEG" > "OrderedGroup.minus_minus"
     2.7 -  "REAL_MUL_SYM" > "IntDef.zmult_ac_2"
     2.8 +  "REAL_MUL_SYM" > "Int.zmult_ac_2"
     2.9    "REAL_MUL_RZERO" > "Ring_and_Field.mult_zero_right"
    2.10    "REAL_MUL_RNEG" > "Ring_and_Field.mult_minus_right"
    2.11    "REAL_MUL_RINV" > "Ring_and_Field.right_inverse"
    2.12 @@ -274,7 +274,7 @@
    2.13    "REAL_ENTIRE" > "Ring_and_Field.field_mult_eq_0_iff"
    2.14    "REAL_DOWN2" > "RealDef.real_lbound_gt_zero"
    2.15    "REAL_DOWN" > "HOL4Real.real.REAL_DOWN"
    2.16 -  "REAL_DOUBLE" > "IntArith.mult_2"
    2.17 +  "REAL_DOUBLE" > "Int.mult_2"
    2.18    "REAL_DIV_RMUL" > "HOL4Real.real.REAL_DIV_RMUL"
    2.19    "REAL_DIV_REFL" > "Ring_and_Field.divide_self"
    2.20    "REAL_DIV_MUL2" > "HOL4Real.real.REAL_DIV_MUL2"
    2.21 @@ -300,7 +300,7 @@
    2.22    "REAL_ABS_TRIANGLE" > "OrderedGroup.abs_triangle_ineq"
    2.23    "REAL_ABS_POS" > "OrderedGroup.abs_ge_zero"
    2.24    "REAL_ABS_MUL" > "Ring_and_Field.abs_mult"
    2.25 -  "REAL_ABS_0" > "Numeral.bin_arith_simps_28"
    2.26 +  "REAL_ABS_0" > "Int.bin_arith_simps_28"
    2.27    "REAL_10" > "HOL4Compat.REAL_10"
    2.28    "REAL_1" > "HOL4Real.real.REAL_1"
    2.29    "REAL_0" > "HOL4Real.real.REAL_0"
    2.30 @@ -353,7 +353,7 @@
    2.31    "ABS_BETWEEN1" > "HOL4Real.real.ABS_BETWEEN1"
    2.32    "ABS_BETWEEN" > "HOL4Real.real.ABS_BETWEEN"
    2.33    "ABS_ABS" > "OrderedGroup.abs_idempotent"
    2.34 -  "ABS_1" > "Numeral.bin_arith_simps_29"
    2.35 -  "ABS_0" > "Numeral.bin_arith_simps_28"
    2.36 +  "ABS_1" > "Int.bin_arith_simps_29"
    2.37 +  "ABS_0" > "Int.bin_arith_simps_28"
    2.38  
    2.39  end
     3.1 --- a/src/HOL/Import/HOL/realax.imp	Mon Jan 21 08:43:29 2008 +0100
     3.2 +++ b/src/HOL/Import/HOL/realax.imp	Mon Jan 21 08:43:30 2008 +0100
     3.3 @@ -91,7 +91,7 @@
     3.4    "TREAL_ADD_ASSOC" > "HOL4Real.realax.TREAL_ADD_ASSOC"
     3.5    "TREAL_10" > "HOL4Real.realax.TREAL_10"
     3.6    "REAL_SUP_ALLPOS" > "HOL4Compat.REAL_SUP_ALLPOS"
     3.7 -  "REAL_MUL_SYM" > "IntDef.zmult_ac_2"
     3.8 +  "REAL_MUL_SYM" > "Int.zmult_ac_2"
     3.9    "REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV"
    3.10    "REAL_MUL_LID" > "Finite_Set.AC_mult.f_e.left_ident"
    3.11    "REAL_MUL_ASSOC" > "HOL4Compat.REAL_MUL_ASSOC"
     4.1 --- a/src/HOL/Import/HOLLight/hollight.imp	Mon Jan 21 08:43:29 2008 +0100
     4.2 +++ b/src/HOL/Import/HOLLight/hollight.imp	Mon Jan 21 08:43:30 2008 +0100
     4.3 @@ -1105,13 +1105,13 @@
     4.4    "NADD_ADD_ASSOC" > "HOLLight.hollight.NADD_ADD_ASSOC"
     4.5    "NADD_ADDITIVE" > "HOLLight.hollight.NADD_ADDITIVE"
     4.6    "NADD_ADD" > "HOLLight.hollight.NADD_ADD"
     4.7 -  "MULT_SYM" > "IntDef.zmult_ac_2"
     4.8 +  "MULT_SYM" > "Int.zmult_ac_2"
     4.9    "MULT_SUC" > "Nat.mult_Suc_right"
    4.10    "MULT_EXP" > "HOLLight.hollight.MULT_EXP"
    4.11    "MULT_EQ_1" > "HOLLight.hollight.MULT_EQ_1"
    4.12    "MULT_EQ_0" > "Nat.mult_is_0"
    4.13    "MULT_CLAUSES" > "HOLLight.hollight.MULT_CLAUSES"
    4.14 -  "MULT_ASSOC" > "IntDef.zmult_ac_1"
    4.15 +  "MULT_ASSOC" > "Int.zmult_ac_1"
    4.16    "MULT_AC" > "HOLLight.hollight.MULT_AC"
    4.17    "MULT_2" > "HOLLight.hollight.MULT_2"
    4.18    "MULT_0" > "Nat.mult_0_right"