--- a/src/HOL/Import/HOL/arithmetic.imp Mon Jan 21 08:43:29 2008 +0100
+++ b/src/HOL/Import/HOL/arithmetic.imp Mon Jan 21 08:43:30 2008 +0100
@@ -108,7 +108,7 @@
"NOT_GREATER" > "Nat.le_def"
"NOT_EXP_0" > "HOL4Base.arithmetic.NOT_EXP_0"
"NORM_0" > "HOL4Base.arithmetic.NORM_0"
- "MULT_SYM" > "IntDef.zmult_ac_2"
+ "MULT_SYM" > "Int.zmult_ac_2"
"MULT_SUC_EQ" > "HOL4Base.arithmetic.MULT_SUC_EQ"
"MULT_SUC" > "Nat.mult_Suc_right"
"MULT_RIGHT_1" > "Finite_Set.AC_mult.f_e.ident"
@@ -120,9 +120,9 @@
"MULT_EQ_1" > "HOL4Base.arithmetic.MULT_EQ_1"
"MULT_EQ_0" > "Nat.mult_is_0"
"MULT_DIV" > "Divides.div_mult_self_is_m"
- "MULT_COMM" > "IntDef.zmult_ac_2"
+ "MULT_COMM" > "Int.zmult_ac_2"
"MULT_CLAUSES" > "HOL4Base.arithmetic.MULT_CLAUSES"
- "MULT_ASSOC" > "IntDef.zmult_ac_1"
+ "MULT_ASSOC" > "Int.zmult_ac_1"
"MULT_0" > "Nat.mult_0_right"
"MULT" > "HOL4Compat.MULT"
"MOD_UNIQUE" > "HOL4Base.arithmetic.MOD_UNIQUE"
--- a/src/HOL/Import/HOL/real.imp Mon Jan 21 08:43:29 2008 +0100
+++ b/src/HOL/Import/HOL/real.imp Mon Jan 21 08:43:30 2008 +0100
@@ -129,7 +129,7 @@
"REAL_NEG_ADD" > "OrderedGroup.minus_add_distrib"
"REAL_NEG_0" > "OrderedGroup.minus_zero"
"REAL_NEGNEG" > "OrderedGroup.minus_minus"
- "REAL_MUL_SYM" > "IntDef.zmult_ac_2"
+ "REAL_MUL_SYM" > "Int.zmult_ac_2"
"REAL_MUL_RZERO" > "Ring_and_Field.mult_zero_right"
"REAL_MUL_RNEG" > "Ring_and_Field.mult_minus_right"
"REAL_MUL_RINV" > "Ring_and_Field.right_inverse"
@@ -274,7 +274,7 @@
"REAL_ENTIRE" > "Ring_and_Field.field_mult_eq_0_iff"
"REAL_DOWN2" > "RealDef.real_lbound_gt_zero"
"REAL_DOWN" > "HOL4Real.real.REAL_DOWN"
- "REAL_DOUBLE" > "IntArith.mult_2"
+ "REAL_DOUBLE" > "Int.mult_2"
"REAL_DIV_RMUL" > "HOL4Real.real.REAL_DIV_RMUL"
"REAL_DIV_REFL" > "Ring_and_Field.divide_self"
"REAL_DIV_MUL2" > "HOL4Real.real.REAL_DIV_MUL2"
@@ -300,7 +300,7 @@
"REAL_ABS_TRIANGLE" > "OrderedGroup.abs_triangle_ineq"
"REAL_ABS_POS" > "OrderedGroup.abs_ge_zero"
"REAL_ABS_MUL" > "Ring_and_Field.abs_mult"
- "REAL_ABS_0" > "Numeral.bin_arith_simps_28"
+ "REAL_ABS_0" > "Int.bin_arith_simps_28"
"REAL_10" > "HOL4Compat.REAL_10"
"REAL_1" > "HOL4Real.real.REAL_1"
"REAL_0" > "HOL4Real.real.REAL_0"
@@ -353,7 +353,7 @@
"ABS_BETWEEN1" > "HOL4Real.real.ABS_BETWEEN1"
"ABS_BETWEEN" > "HOL4Real.real.ABS_BETWEEN"
"ABS_ABS" > "OrderedGroup.abs_idempotent"
- "ABS_1" > "Numeral.bin_arith_simps_29"
- "ABS_0" > "Numeral.bin_arith_simps_28"
+ "ABS_1" > "Int.bin_arith_simps_29"
+ "ABS_0" > "Int.bin_arith_simps_28"
end
--- a/src/HOL/Import/HOL/realax.imp Mon Jan 21 08:43:29 2008 +0100
+++ b/src/HOL/Import/HOL/realax.imp Mon Jan 21 08:43:30 2008 +0100
@@ -91,7 +91,7 @@
"TREAL_ADD_ASSOC" > "HOL4Real.realax.TREAL_ADD_ASSOC"
"TREAL_10" > "HOL4Real.realax.TREAL_10"
"REAL_SUP_ALLPOS" > "HOL4Compat.REAL_SUP_ALLPOS"
- "REAL_MUL_SYM" > "IntDef.zmult_ac_2"
+ "REAL_MUL_SYM" > "Int.zmult_ac_2"
"REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV"
"REAL_MUL_LID" > "Finite_Set.AC_mult.f_e.left_ident"
"REAL_MUL_ASSOC" > "HOL4Compat.REAL_MUL_ASSOC"
--- a/src/HOL/Import/HOLLight/hollight.imp Mon Jan 21 08:43:29 2008 +0100
+++ b/src/HOL/Import/HOLLight/hollight.imp Mon Jan 21 08:43:30 2008 +0100
@@ -1105,13 +1105,13 @@
"NADD_ADD_ASSOC" > "HOLLight.hollight.NADD_ADD_ASSOC"
"NADD_ADDITIVE" > "HOLLight.hollight.NADD_ADDITIVE"
"NADD_ADD" > "HOLLight.hollight.NADD_ADD"
- "MULT_SYM" > "IntDef.zmult_ac_2"
+ "MULT_SYM" > "Int.zmult_ac_2"
"MULT_SUC" > "Nat.mult_Suc_right"
"MULT_EXP" > "HOLLight.hollight.MULT_EXP"
"MULT_EQ_1" > "HOLLight.hollight.MULT_EQ_1"
"MULT_EQ_0" > "Nat.mult_is_0"
"MULT_CLAUSES" > "HOLLight.hollight.MULT_CLAUSES"
- "MULT_ASSOC" > "IntDef.zmult_ac_1"
+ "MULT_ASSOC" > "Int.zmult_ac_1"
"MULT_AC" > "HOLLight.hollight.MULT_AC"
"MULT_2" > "HOLLight.hollight.MULT_2"
"MULT_0" > "Nat.mult_0_right"