--- a/src/HOL/Import/HOLLight/hollight.imp Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Import/HOLLight/hollight.imp Fri Mar 10 15:33:48 2006 +0100
@@ -238,10 +238,10 @@
"<=" > "HOLLight.hollight.<="
"<" > "HOLLight.hollight.<"
"/\\" > "op &"
- "-" > "op -" :: "nat => nat => nat"
+ "-" > "HOL.minus" :: "nat => nat => nat"
"," > "Pair"
- "+" > "op +" :: "nat => nat => nat"
- "*" > "op *" :: "nat => nat => nat"
+ "+" > "HOL.plus" :: "nat => nat => nat"
+ "*" > "HOL.times" :: "nat => nat => nat"
"$" > "HOLLight.hollight.$"
"!" > "All"