src/HOL/Import/HOL/arithmetic.imp

   "NOT_LEQ" > "HOL4Base.arithmetic.NOT_LEQ"
   "NOT_GREATER_EQ" > "HOL4Base.arithmetic.NOT_GREATER_EQ"
   "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"
   "MULT_MONO_EQ" > "Nat.Suc_mult_cancel1"
   "MULT_LESS_EQ_SUC" > "Nat.Suc_mult_le_cancel1"

   "MULT_INCREASES" > "HOL4Base.arithmetic.MULT_INCREASES"
   "MULT_EXP_MONO" > "HOL4Base.arithmetic.MULT_EXP_MONO"
   "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"
   "MOD_TIMES2" > "HOL4Base.arithmetic.MOD_TIMES2"
   "MOD_TIMES" > "HOL4Base.arithmetic.MOD_TIMES"