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