diff -r f0285e69d704 -r 3d3d8f8929a7 src/HOL/Import/HOL4/Generated/operator.imp
--- /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