src/HOL/Import/HOLLight/hollight.imp
changeset 25930 83e3dd60affe
parent 22997 d4f3b015b50b
child 30925 c38cbc0ac8d1
--- 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"