--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/HOL4/Generated/operator.imp Sat Mar 03 22:37:41 2012 +0100
@@ -0,0 +1,40 @@
+import
+
+import_segment "hol4"
+
+def_maps
+ "RIGHT_ID" > "RIGHT_ID_def"
+ "MONOID" > "MONOID_def"
+ "LEFT_ID" > "LEFT_ID_def"
+ "FCOMM" > "FCOMM_def"
+ "COMM" > "COMM_def"
+ "ASSOC" > "ASSOC_def"
+
+const_maps
+ "RIGHT_ID" > "HOL4Base.operator.RIGHT_ID"
+ "MONOID" > "HOL4Base.operator.MONOID"
+ "LEFT_ID" > "HOL4Base.operator.LEFT_ID"
+ "FCOMM" > "HOL4Base.operator.FCOMM"
+ "COMM" > "HOL4Base.operator.COMM"
+ "ASSOC" > "HOL4Base.operator.ASSOC"
+
+thm_maps
+ "RIGHT_ID_def" > "HOL4Base.operator.RIGHT_ID_def"
+ "RIGHT_ID_DEF" > "HOL4Base.operator.RIGHT_ID_DEF"
+ "MONOID_def" > "HOL4Base.operator.MONOID_def"
+ "MONOID_DISJ_F" > "HOL4Base.operator.MONOID_DISJ_F"
+ "MONOID_DEF" > "HOL4Base.operator.MONOID_DEF"
+ "MONOID_CONJ_T" > "HOL4Base.operator.MONOID_CONJ_T"
+ "LEFT_ID_def" > "HOL4Base.operator.LEFT_ID_def"
+ "LEFT_ID_DEF" > "HOL4Base.operator.LEFT_ID_DEF"
+ "FCOMM_def" > "HOL4Base.operator.FCOMM_def"
+ "FCOMM_DEF" > "HOL4Base.operator.FCOMM_DEF"
+ "FCOMM_ASSOC" > "HOL4Base.operator.FCOMM_ASSOC"
+ "COMM_def" > "HOL4Base.operator.COMM_def"
+ "COMM_DEF" > "HOL4Base.operator.COMM_DEF"
+ "ASSOC_def" > "HOL4Base.operator.ASSOC_def"
+ "ASSOC_DISJ" > "HOL4Base.operator.ASSOC_DISJ"
+ "ASSOC_DEF" > "HOL4Base.operator.ASSOC_DEF"
+ "ASSOC_CONJ" > "HOL4Base.operator.ASSOC_CONJ"
+
+end