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