--- 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"