src/HOL/Import/HOL/state_transformer.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   "UNIT" > "UNIT_def"
     7   "MMAP" > "MMAP_def"
     8   "JOIN" > "JOIN_def"
     9   "BIND" > "BIND_def"
    10 
    11 const_maps
    12   "UNIT" > "HOL4Base.state_transformer.UNIT"
    13   "MMAP" > "HOL4Base.state_transformer.MMAP"
    14   "JOIN" > "HOL4Base.state_transformer.JOIN"
    15   "BIND" > "HOL4Base.state_transformer.BIND"
    16 
    17 thm_maps
    18   "UNIT_def" > "HOL4Base.state_transformer.UNIT_def"
    19   "UNIT_UNCURRY" > "HOL4Base.state_transformer.UNIT_UNCURRY"
    20   "UNIT_DEF" > "HOL4Base.state_transformer.UNIT_DEF"
    21   "SND_o_UNIT" > "HOL4Base.state_transformer.SND_o_UNIT"
    22   "MMAP_def" > "HOL4Base.state_transformer.MMAP_def"
    23   "MMAP_UNIT" > "HOL4Base.state_transformer.MMAP_UNIT"
    24   "MMAP_JOIN" > "HOL4Base.state_transformer.MMAP_JOIN"
    25   "MMAP_ID" > "HOL4Base.state_transformer.MMAP_ID"
    26   "MMAP_DEF" > "HOL4Base.state_transformer.MMAP_DEF"
    27   "MMAP_COMP" > "HOL4Base.state_transformer.MMAP_COMP"
    28   "JOIN_def" > "HOL4Base.state_transformer.JOIN_def"
    29   "JOIN_UNIT" > "HOL4Base.state_transformer.JOIN_UNIT"
    30   "JOIN_MMAP_UNIT" > "HOL4Base.state_transformer.JOIN_MMAP_UNIT"
    31   "JOIN_MAP_JOIN" > "HOL4Base.state_transformer.JOIN_MAP_JOIN"
    32   "JOIN_MAP" > "HOL4Base.state_transformer.JOIN_MAP"
    33   "JOIN_DEF" > "HOL4Base.state_transformer.JOIN_DEF"
    34   "FST_o_UNIT" > "HOL4Base.state_transformer.FST_o_UNIT"
    35   "FST_o_MMAP" > "HOL4Base.state_transformer.FST_o_MMAP"
    36   "BIND_def" > "HOL4Base.state_transformer.BIND_def"
    37   "BIND_RIGHT_UNIT" > "HOL4Base.state_transformer.BIND_RIGHT_UNIT"
    38   "BIND_LEFT_UNIT" > "HOL4Base.state_transformer.BIND_LEFT_UNIT"
    39   "BIND_DEF" > "HOL4Base.state_transformer.BIND_DEF"
    40   "BIND_ASSOC" > "HOL4Base.state_transformer.BIND_ASSOC"
    41 
    42 end