src/HOL/Import/HOL/operator.imp
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 14516 a183dec876ab
permissions -rw-r--r--
adaptions to codegen_package
     1 import
     2 
     3 import_segment "hol4"
     4 
     5 def_maps
     6   "RIGHT_ID" > "RIGHT_ID_def"
     7   "MONOID" > "MONOID_def"
     8   "LEFT_ID" > "LEFT_ID_def"
     9   "FCOMM" > "FCOMM_def"
    10   "COMM" > "COMM_def"
    11   "ASSOC" > "ASSOC_def"
    12 
    13 const_maps
    14   "RIGHT_ID" > "HOL4Base.operator.RIGHT_ID"
    15   "MONOID" > "HOL4Base.operator.MONOID"
    16   "LEFT_ID" > "HOL4Base.operator.LEFT_ID"
    17   "FCOMM" > "HOL4Base.operator.FCOMM"
    18   "COMM" > "HOL4Base.operator.COMM"
    19   "ASSOC" > "HOL4Base.operator.ASSOC"
    20 
    21 thm_maps
    22   "RIGHT_ID_def" > "HOL4Base.operator.RIGHT_ID_def"
    23   "RIGHT_ID_DEF" > "HOL4Base.operator.RIGHT_ID_DEF"
    24   "MONOID_def" > "HOL4Base.operator.MONOID_def"
    25   "MONOID_DISJ_F" > "HOL4Base.operator.MONOID_DISJ_F"
    26   "MONOID_DEF" > "HOL4Base.operator.MONOID_DEF"
    27   "MONOID_CONJ_T" > "HOL4Base.operator.MONOID_CONJ_T"
    28   "LEFT_ID_def" > "HOL4Base.operator.LEFT_ID_def"
    29   "LEFT_ID_DEF" > "HOL4Base.operator.LEFT_ID_DEF"
    30   "FCOMM_def" > "HOL4Base.operator.FCOMM_def"
    31   "FCOMM_DEF" > "HOL4Base.operator.FCOMM_DEF"
    32   "FCOMM_ASSOC" > "HOL4Base.operator.FCOMM_ASSOC"
    33   "COMM_def" > "HOL4Base.operator.COMM_def"
    34   "COMM_DEF" > "HOL4Base.operator.COMM_DEF"
    35   "ASSOC_def" > "HOL4Base.operator.ASSOC_def"
    36   "ASSOC_DISJ" > "HOL4Base.operator.ASSOC_DISJ"
    37   "ASSOC_DEF" > "HOL4Base.operator.ASSOC_DEF"
    38   "ASSOC_CONJ" > "HOL4Base.operator.ASSOC_CONJ"
    39 
    40 end