src/HOL/Import/HOLLight/hollight.imp
changeset 38795 848be46708dc
parent 38786 e46e7a9cb622
child 38864 4abe644fcea5
--- a/src/HOL/Import/HOLLight/hollight.imp	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp	Fri Aug 27 10:56:46 2010 +0200
@@ -115,7 +115,7 @@
   "_10303" > "HOLLight.hollight._10303"
   "_10302" > "HOLLight.hollight._10302"
   "_0" > "0" :: "nat"
-  "\\/" > "op |"
+  "\\/" > HOL.disj
   "ZRECSPACE" > "HOLLight.hollight.ZRECSPACE"
   "ZIP" > "HOLLight.hollight.ZIP"
   "ZCONSTR" > "HOLLight.hollight.ZCONSTR"
@@ -237,7 +237,7 @@
   "=" > "op ="
   "<=" > "HOLLight.hollight.<="
   "<" > "HOLLight.hollight.<"
-  "/\\" > "op &"
+  "/\\" > HOL.conj
   "-" > "Groups.minus" :: "nat => nat => nat"
   "," > "Product_Type.Pair"
   "+" > "Groups.plus" :: "nat => nat => nat"