src/HOL/Import/HOL/ind_type.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   "mk_rec" > "mk_rec_def"
     7   "dest_rec" > "dest_rec_def"
     8   "ZRECSPACE" > "ZRECSPACE_def"
     9   "ZCONSTR" > "ZCONSTR_def"
    10   "ZBOT" > "ZBOT_def"
    11   "NUMSUM" > "NUMSUM_def"
    12   "NUMSND" > "NUMSND_def"
    13   "NUMRIGHT" > "NUMRIGHT_def"
    14   "NUMPAIR" > "NUMPAIR_def"
    15   "NUMLEFT" > "NUMLEFT_def"
    16   "NUMFST" > "NUMFST_def"
    17   "ISO" > "ISO_def"
    18   "INJP" > "INJP_def"
    19   "INJN" > "INJN_def"
    20   "INJF" > "INJF_def"
    21   "INJA" > "INJA_def"
    22   "FNIL" > "FNIL_def"
    23   "FCONS" > "FCONS_def"
    24   "CONSTR" > "CONSTR_def"
    25   "BOTTOM" > "BOTTOM_def"
    26 
    27 type_maps
    28   "recspace" > "HOL4Base.ind_type.recspace"
    29 
    30 const_maps
    31   "ZRECSPACE" > "HOL4Base.ind_type.ZRECSPACE"
    32   "ZCONSTR" > "HOL4Base.ind_type.ZCONSTR"
    33   "ZBOT" > "HOL4Base.ind_type.ZBOT"
    34   "NUMSUM" > "HOL4Base.ind_type.NUMSUM"
    35   "NUMPAIR" > "HOL4Base.ind_type.NUMPAIR"
    36   "ISO" > "HOL4Base.ind_type.ISO"
    37   "INJP" > "HOL4Base.ind_type.INJP"
    38   "INJN" > "HOL4Base.ind_type.INJN"
    39   "INJF" > "HOL4Base.ind_type.INJF"
    40   "INJA" > "HOL4Base.ind_type.INJA"
    41   "FNIL" > "HOL4Base.ind_type.FNIL"
    42   "CONSTR" > "HOL4Base.ind_type.CONSTR"
    43   "BOTTOM" > "HOL4Base.ind_type.BOTTOM"
    44 
    45 thm_maps
    46   "recspace_repfns" > "HOL4Base.ind_type.recspace_repfns"
    47   "recspace_TY_DEF" > "HOL4Base.ind_type.recspace_TY_DEF"
    48   "ZRECSPACE_rules" > "HOL4Base.ind_type.ZRECSPACE_rules"
    49   "ZRECSPACE_ind" > "HOL4Base.ind_type.ZRECSPACE_ind"
    50   "ZRECSPACE_def" > "HOL4Base.ind_type.ZRECSPACE_def"
    51   "ZRECSPACE_cases" > "HOL4Base.ind_type.ZRECSPACE_cases"
    52   "ZRECSPACE" > "HOL4Base.ind_type.ZRECSPACE"
    53   "ZCONSTR_def" > "HOL4Base.ind_type.ZCONSTR_def"
    54   "ZCONSTR_ZBOT" > "HOL4Base.ind_type.ZCONSTR_ZBOT"
    55   "ZCONSTR" > "HOL4Base.ind_type.ZCONSTR"
    56   "ZBOT_def" > "HOL4Base.ind_type.ZBOT_def"
    57   "ZBOT" > "HOL4Base.ind_type.ZBOT"
    58   "NUMSUM_def" > "HOL4Base.ind_type.NUMSUM_def"
    59   "NUMSUM_INJ" > "HOL4Base.ind_type.NUMSUM_INJ"
    60   "NUMSUM_DEST" > "HOL4Base.ind_type.NUMSUM_DEST"
    61   "NUMSUM" > "HOL4Base.ind_type.NUMSUM"
    62   "NUMPAIR_def" > "HOL4Base.ind_type.NUMPAIR_def"
    63   "NUMPAIR_INJ_LEMMA" > "HOL4Base.ind_type.NUMPAIR_INJ_LEMMA"
    64   "NUMPAIR_INJ" > "HOL4Base.ind_type.NUMPAIR_INJ"
    65   "NUMPAIR_DEST" > "HOL4Base.ind_type.NUMPAIR_DEST"
    66   "NUMPAIR" > "HOL4Base.ind_type.NUMPAIR"
    67   "MK_REC_INJ" > "HOL4Base.ind_type.MK_REC_INJ"
    68   "ISO_def" > "HOL4Base.ind_type.ISO_def"
    69   "ISO_USAGE" > "HOL4Base.ind_type.ISO_USAGE"
    70   "ISO_REFL" > "HOL4Base.ind_type.ISO_REFL"
    71   "ISO_FUN" > "HOL4Base.ind_type.ISO_FUN"
    72   "ISO" > "HOL4Base.ind_type.ISO"
    73   "INJ_INVERSE2" > "HOL4Base.ind_type.INJ_INVERSE2"
    74   "INJP_def" > "HOL4Base.ind_type.INJP_def"
    75   "INJP_INJ" > "HOL4Base.ind_type.INJP_INJ"
    76   "INJP" > "HOL4Base.ind_type.INJP"
    77   "INJN_def" > "HOL4Base.ind_type.INJN_def"
    78   "INJN_INJ" > "HOL4Base.ind_type.INJN_INJ"
    79   "INJN" > "HOL4Base.ind_type.INJN"
    80   "INJF_def" > "HOL4Base.ind_type.INJF_def"
    81   "INJF_INJ" > "HOL4Base.ind_type.INJF_INJ"
    82   "INJF" > "HOL4Base.ind_type.INJF"
    83   "INJA_def" > "HOL4Base.ind_type.INJA_def"
    84   "INJA_INJ" > "HOL4Base.ind_type.INJA_INJ"
    85   "INJA" > "HOL4Base.ind_type.INJA"
    86   "FNIL_def" > "HOL4Base.ind_type.FNIL_def"
    87   "FNIL" > "HOL4Base.ind_type.FNIL"
    88   "FCONS" > "HOL4Base.ind_type.FCONS"
    89   "DEST_REC_INJ" > "HOL4Base.ind_type.DEST_REC_INJ"
    90   "CONSTR_def" > "HOL4Base.ind_type.CONSTR_def"
    91   "CONSTR_REC" > "HOL4Base.ind_type.CONSTR_REC"
    92   "CONSTR_INJ" > "HOL4Base.ind_type.CONSTR_INJ"
    93   "CONSTR_IND" > "HOL4Base.ind_type.CONSTR_IND"
    94   "CONSTR_BOT" > "HOL4Base.ind_type.CONSTR_BOT"
    95   "CONSTR" > "HOL4Base.ind_type.CONSTR"
    96   "BOTTOM_def" > "HOL4Base.ind_type.BOTTOM_def"
    97   "BOTTOM" > "HOL4Base.ind_type.BOTTOM"
    98 
    99 end