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