src/HOL/Import/HOLLight/hollight.imp
changeset 19233 77ca20b0ed77
parent 19093 6d584f9d2021
child 22997 d4f3b015b50b
--- 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"