src/HOL/Import/HOL/bool.imp
changeset 38795 848be46708dc
parent 38556 dc92eee56ed7
child 39198 f967a16dfcdd
--- a/src/HOL/Import/HOL/bool.imp	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Import/HOL/bool.imp	Fri Aug 27 10:56:46 2010 +0200
@@ -14,7 +14,7 @@
 const_maps
   "~" > "HOL.Not"
   "bool_case" > "Datatype.bool.bool_case"
-  "\\/" > "op |"
+  "\\/" > HOL.disj
   "TYPE_DEFINITION" > "HOL4Setup.TYPE_DEFINITION"
   "T" > "HOL.True"
   "RES_SELECT" > "HOL4Base.bool.RES_SELECT"
@@ -30,7 +30,7 @@
   "ARB" > "HOL4Base.bool.ARB"
   "?!" > "HOL.Ex1"
   "?" > "HOL.Ex"
-  "/\\" > "op &"
+  "/\\" > HOL.conj
   "!" > "HOL.All"
 
 thm_maps