src/HOL/Import/HOL/boolean_sequence.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
  "STL" > "STL_primdef"
skalberg@14516
     7
  "STAKE" > "STAKE_primdef"
skalberg@14516
     8
  "SHD" > "SHD_primdef"
skalberg@14516
     9
  "SDROP" > "SDROP_primdef"
skalberg@14516
    10
  "SDEST" > "SDEST_primdef"
skalberg@14516
    11
  "SCONST" > "SCONST_primdef"
skalberg@14516
    12
  "SCONS" > "SCONS_primdef"
skalberg@14516
    13
skalberg@14516
    14
const_maps
skalberg@14516
    15
  "STL" > "HOL4Prob.boolean_sequence.STL"
skalberg@14516
    16
  "SHD" > "HOL4Prob.boolean_sequence.SHD"
skalberg@14516
    17
  "SDEST" > "HOL4Prob.boolean_sequence.SDEST"
skalberg@14516
    18
  "SCONST" > "HOL4Prob.boolean_sequence.SCONST"
skalberg@14516
    19
skalberg@14516
    20
thm_maps
skalberg@14516
    21
  "STL_primdef" > "HOL4Prob.boolean_sequence.STL_primdef"
skalberg@14516
    22
  "STL_def" > "HOL4Prob.boolean_sequence.STL_def"
skalberg@14516
    23
  "STL_SCONST" > "HOL4Prob.boolean_sequence.STL_SCONST"
skalberg@14516
    24
  "STL_SCONS" > "HOL4Prob.boolean_sequence.STL_SCONS"
skalberg@14516
    25
  "STAKE_def" > "HOL4Prob.boolean_sequence.STAKE_def"
skalberg@14516
    26
  "SHD_primdef" > "HOL4Prob.boolean_sequence.SHD_primdef"
skalberg@14516
    27
  "SHD_def" > "HOL4Prob.boolean_sequence.SHD_def"
skalberg@14516
    28
  "SHD_STL_ISO" > "HOL4Prob.boolean_sequence.SHD_STL_ISO"
skalberg@14516
    29
  "SHD_SCONST" > "HOL4Prob.boolean_sequence.SHD_SCONST"
skalberg@14516
    30
  "SHD_SCONS" > "HOL4Prob.boolean_sequence.SHD_SCONS"
skalberg@14516
    31
  "SDROP_def" > "HOL4Prob.boolean_sequence.SDROP_def"
skalberg@14516
    32
  "SDEST_primdef" > "HOL4Prob.boolean_sequence.SDEST_primdef"
skalberg@14516
    33
  "SDEST_def" > "HOL4Prob.boolean_sequence.SDEST_def"
skalberg@14516
    34
  "SCONS_def" > "HOL4Prob.boolean_sequence.SCONS_def"
skalberg@14516
    35
  "SCONS_SURJ" > "HOL4Prob.boolean_sequence.SCONS_SURJ"
skalberg@14516
    36
  "SCONST_primdef" > "HOL4Prob.boolean_sequence.SCONST_primdef"
skalberg@14516
    37
  "SCONST_def" > "HOL4Prob.boolean_sequence.SCONST_def"
skalberg@14516
    38
skalberg@14516
    39
end