--- a/src/HOL/Import/HOL4/Generated/operator.imp Sun Apr 01 14:50:47 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-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