# HG changeset patch
# User haftmann
# Date 1200901410 -3600
# Node ID 83e3dd60affec236a7bc0a92a2113b60549471a9
# Parent  6bfef23e26beb45fc5853999f717e689fc4801eb
adjusted to constant and theorem renames

diff -r 6bfef23e26be -r 83e3dd60affe src/HOL/Import/HOL/arithmetic.imp
--- 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"
diff -r 6bfef23e26be -r 83e3dd60affe src/HOL/Import/HOL/real.imp
--- 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
diff -r 6bfef23e26be -r 83e3dd60affe src/HOL/Import/HOL/realax.imp
--- 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"
diff -r 6bfef23e26be -r 83e3dd60affe src/HOL/Import/HOLLight/hollight.imp
--- 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"