src/HOL/Import/HOL/sum.imp
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 15647 b1f486a9c56b
child 44763 b50d5d694838
permissions -rw-r--r--
adaptions to codegen_package
     1 import
     2 
     3 import_segment "hol4"
     4 
     5 type_maps
     6   "sum" > "+"
     7 
     8 const_maps
     9   "sum_case" > "Datatype.sum.sum_case"
    10   "OUTR" > "HOL4Compat.OUTR"
    11   "OUTL" > "HOL4Compat.OUTL"
    12   "ISR" > "HOL4Compat.ISR"
    13   "ISL" > "HOL4Compat.ISL"
    14   "INR" > "Sum_Type.Inr"
    15   "INL" > "Sum_Type.Inl"
    16 
    17 thm_maps
    18   "sum_distinct1" > "Datatype.sum.simps_2"
    19   "sum_distinct" > "Datatype.sum.simps_1"
    20   "sum_case_def" > "HOL4Compat.sum_case_def"
    21   "sum_case_cong" > "HOL4Base.sum.sum_case_cong"
    22   "sum_INDUCT" > "HOL4Compat.OUTR.induct"
    23   "sum_CASES" > "Datatype.sum.nchotomy"
    24   "OUTR" > "HOL4Compat.OUTR"
    25   "OUTL" > "HOL4Compat.OUTL"
    26   "ISR" > "HOL4Compat.ISR"
    27   "ISL_OR_ISR" > "HOL4Base.sum.ISL_OR_ISR"
    28   "ISL" > "HOL4Compat.ISL"
    29   "INR_neq_INL" > "Datatype.sum.simps_2"
    30   "INR_INL_11" > "HOL4Compat.INR_INL_11"
    31   "INR" > "HOL4Base.sum.INR"
    32   "INL" > "HOL4Base.sum.INL"
    33 
    34 ignore_thms
    35   "sum_axiom"
    36   "sum_TY_DEF"
    37   "sum_ISO_DEF"
    38   "sum_Axiom"
    39   "IS_SUM_REP"
    40   "INR_DEF"
    41   "INL_DEF"
    42 
    43 end