src/HOL/Import/HOL/list.imp
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 14516 a183dec876ab
child 22997 d4f3b015b50b
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
  "EL" > "EL_def"
skalberg@14516
     7
skalberg@14516
     8
type_maps
skalberg@14516
     9
  "list" > "List.list"
skalberg@14516
    10
skalberg@14516
    11
const_maps
skalberg@14516
    12
  "list_size" > "HOL4Compat.list_size"
skalberg@14516
    13
  "list_case" > "List.list.list_case"
skalberg@14516
    14
  "ZIP" > "HOL4Compat.ZIP"
skalberg@14516
    15
  "UNZIP" > "HOL4Compat.unzip"
skalberg@14516
    16
  "TL" > "List.tl"
skalberg@14516
    17
  "SUM" > "HOL4Compat.sum"
skalberg@14516
    18
  "REVERSE" > "List.rev"
skalberg@14516
    19
  "REPLICATE" > "List.replicate"
skalberg@14516
    20
  "NULL" > "List.null"
skalberg@14516
    21
  "NIL" > "List.list.Nil"
skalberg@14516
    22
  "MEM" > "List.op mem"
skalberg@14516
    23
  "MAP2" > "HOL4Compat.map2"
skalberg@14516
    24
  "MAP" > "List.map"
skalberg@14516
    25
  "LENGTH" > "Nat.size"
skalberg@14516
    26
  "LAST" > "List.last"
skalberg@14516
    27
  "HD" > "List.hd"
skalberg@14516
    28
  "FRONT" > "List.butlast"
skalberg@14516
    29
  "FOLDR" > "HOL4Compat.FOLDR"
skalberg@14516
    30
  "FOLDL" > "List.foldl"
skalberg@14516
    31
  "FLAT" > "List.concat"
skalberg@14516
    32
  "FILTER" > "List.filter"
skalberg@14516
    33
  "EXISTS" > "HOL4Compat.list_exists"
skalberg@14516
    34
  "EVERY" > "List.list_all"
skalberg@14516
    35
  "CONS" > "List.list.Cons"
skalberg@14516
    36
  "APPEND" > "List.op @"
skalberg@14516
    37
skalberg@14516
    38
thm_maps
skalberg@14516
    39
  "list_size_def" > "HOL4Compat.list_size_def"
skalberg@14516
    40
  "list_size_cong" > "HOL4Base.list.list_size_cong"
skalberg@14516
    41
  "list_nchotomy" > "HOL4Compat.list_CASES"
skalberg@14516
    42
  "list_induction" > "HOL4Compat.unzip.induct"
skalberg@14516
    43
  "list_distinct" > "List.list.simps_1"
skalberg@14516
    44
  "list_case_def" > "HOL4Compat.list_case_def"
skalberg@14516
    45
  "list_case_cong" > "HOL4Compat.list_case_cong"
skalberg@14516
    46
  "list_case_compute" > "HOL4Base.list.list_case_compute"
skalberg@14516
    47
  "list_INDUCT" > "HOL4Compat.unzip.induct"
skalberg@14516
    48
  "list_CASES" > "HOL4Compat.list_CASES"
skalberg@14516
    49
  "list_Axiom_old" > "HOL4Compat.list_Axiom_old"
skalberg@14516
    50
  "list_Axiom" > "HOL4Compat.list_Axiom"
skalberg@14516
    51
  "list_11" > "List.list.simps_3"
skalberg@14516
    52
  "ZIP_UNZIP" > "HOL4Base.list.ZIP_UNZIP"
skalberg@14516
    53
  "ZIP_MAP" > "HOL4Base.list.ZIP_MAP"
skalberg@14516
    54
  "ZIP" > "HOL4Compat.ZIP"
skalberg@14516
    55
  "WF_LIST_PRED" > "HOL4Base.list.WF_LIST_PRED"
skalberg@14516
    56
  "UNZIP_ZIP" > "HOL4Base.list.UNZIP_ZIP"
skalberg@14516
    57
  "UNZIP" > "HOL4Compat.UNZIP"
skalberg@14516
    58
  "TL" > "List.tl.simps_2"
skalberg@14516
    59
  "SUM" > "HOL4Compat.SUM"
skalberg@14516
    60
  "REVERSE_REVERSE" > "List.rev_rev_ident"
skalberg@14516
    61
  "REVERSE_DEF" > "HOL4Compat.REVERSE"
skalberg@14516
    62
  "REVERSE_APPEND" > "List.rev_append"
skalberg@14516
    63
  "NULL_DEF" > "HOL4Compat.NULL_DEF"
skalberg@14516
    64
  "NULL" > "HOL4Base.list.NULL"
skalberg@14516
    65
  "NOT_NIL_CONS" > "List.list.simps_1"
skalberg@14516
    66
  "NOT_EXISTS" > "HOL4Base.list.NOT_EXISTS"
skalberg@14516
    67
  "NOT_EVERY" > "HOL4Base.list.NOT_EVERY"
skalberg@14516
    68
  "NOT_EQ_LIST" > "HOL4Base.list.NOT_EQ_LIST"
skalberg@14516
    69
  "NOT_CONS_NIL" > "List.list.simps_2"
skalberg@14516
    70
  "MEM_ZIP" > "HOL4Base.list.MEM_ZIP"
skalberg@14516
    71
  "MEM_MAP" > "HOL4Base.list.MEM_MAP"
skalberg@14516
    72
  "MEM_EL" > "HOL4Base.list.MEM_EL"
skalberg@14516
    73
  "MEM_APPEND" > "HOL4Base.list.MEM_APPEND"
skalberg@14516
    74
  "MEM" > "HOL4Compat.MEM"
skalberg@14516
    75
  "MAP_EQ_NIL" > "HOL4Base.list.MAP_EQ_NIL"
skalberg@14516
    76
  "MAP_CONG" > "HOL4Base.list.MAP_CONG"
skalberg@14516
    77
  "MAP_APPEND" > "List.map_append"
skalberg@14516
    78
  "MAP2_ZIP" > "HOL4Base.list.MAP2_ZIP"
skalberg@14516
    79
  "MAP2" > "HOL4Compat.MAP2"
skalberg@14516
    80
  "MAP" > "HOL4Compat.MAP"
skalberg@14516
    81
  "LIST_NOT_EQ" > "HOL4Base.list.LIST_NOT_EQ"
skalberg@14516
    82
  "LENGTH_ZIP" > "HOL4Base.list.LENGTH_ZIP"
skalberg@14516
    83
  "LENGTH_UNZIP" > "HOL4Base.list.LENGTH_UNZIP"
skalberg@14516
    84
  "LENGTH_NIL" > "List.length_0_conv"
skalberg@14516
    85
  "LENGTH_MAP" > "List.length_map"
skalberg@14516
    86
  "LENGTH_EQ_NIL" > "HOL4Base.list.LENGTH_EQ_NIL"
skalberg@14516
    87
  "LENGTH_EQ_CONS" > "HOL4Base.list.LENGTH_EQ_CONS"
skalberg@14516
    88
  "LENGTH_CONS" > "HOL4Base.list.LENGTH_CONS"
skalberg@14516
    89
  "LENGTH_APPEND" > "List.length_append"
skalberg@14516
    90
  "LENGTH" > "HOL4Compat.LENGTH"
skalberg@14516
    91
  "LAST_DEF" > "List.last.simps"
skalberg@14516
    92
  "LAST_CONS" > "HOL4Base.list.LAST_CONS"
skalberg@14516
    93
  "HD" > "List.hd.simps"
skalberg@14516
    94
  "FRONT_DEF" > "List.butlast.simps_2"
skalberg@14516
    95
  "FRONT_CONS" > "HOL4Base.list.FRONT_CONS"
skalberg@14516
    96
  "FOLDR_CONG" > "HOL4Base.list.FOLDR_CONG"
skalberg@14516
    97
  "FOLDR" > "HOL4Compat.FOLDR"
skalberg@14516
    98
  "FOLDL_CONG" > "HOL4Base.list.FOLDL_CONG"
skalberg@14516
    99
  "FOLDL" > "HOL4Compat.FOLDL"
skalberg@14516
   100
  "FLAT" > "HOL4Compat.FLAT"
skalberg@14516
   101
  "FILTER" > "HOL4Compat.FILTER"
skalberg@14516
   102
  "EXISTS_MEM" > "HOL4Base.list.EXISTS_MEM"
skalberg@14516
   103
  "EXISTS_DEF" > "HOL4Compat.list_exists_DEF"
skalberg@14516
   104
  "EXISTS_CONG" > "HOL4Base.list.EXISTS_CONG"
skalberg@14516
   105
  "EXISTS_APPEND" > "HOL4Base.list.EXISTS_APPEND"
skalberg@14516
   106
  "EVERY_MONOTONIC" > "HOL4Base.list.EVERY_MONOTONIC"
skalberg@14516
   107
  "EVERY_MEM" > "HOL4Base.list.EVERY_MEM"
skalberg@14516
   108
  "EVERY_EL" > "HOL4Base.list.EVERY_EL"
skalberg@14516
   109
  "EVERY_DEF" > "HOL4Compat.EVERY_DEF"
skalberg@14516
   110
  "EVERY_CONJ" > "HOL4Base.list.EVERY_CONJ"
skalberg@14516
   111
  "EVERY_CONG" > "HOL4Base.list.EVERY_CONG"
skalberg@14516
   112
  "EVERY_APPEND" > "List.list_all_append"
skalberg@14516
   113
  "EQ_LIST" > "HOL4Base.list.EQ_LIST"
skalberg@14516
   114
  "EL_compute" > "HOL4Base.list.EL_compute"
skalberg@14516
   115
  "EL_ZIP" > "HOL4Base.list.EL_ZIP"
skalberg@14516
   116
  "EL" > "HOL4Base.list.EL"
skalberg@14516
   117
  "CONS_ACYCLIC" > "HOL4Base.list.CONS_ACYCLIC"
skalberg@14516
   118
  "CONS_11" > "List.list.simps_3"
skalberg@14516
   119
  "CONS" > "HOL4Base.list.CONS"
skalberg@14516
   120
  "APPEND_eq_NIL" > "HOL4Base.list.APPEND_eq_NIL"
skalberg@14516
   121
  "APPEND_NIL" > "List.append_Nil2"
skalberg@14516
   122
  "APPEND_FRONT_LAST" > "List.append_butlast_last_id"
skalberg@14516
   123
  "APPEND_ASSOC" > "List.append_assoc"
skalberg@14516
   124
  "APPEND_11" > "HOL4Base.list.APPEND_11"
skalberg@14516
   125
  "APPEND" > "HOL4Compat.APPEND"
skalberg@14516
   126
skalberg@14516
   127
ignore_thms
skalberg@14516
   128
  "list_repfns"
skalberg@14516
   129
  "list_TY_DEF"
skalberg@14516
   130
  "list1_def"
skalberg@14516
   131
  "list0_def"
skalberg@14516
   132
  "NIL"
skalberg@14516
   133
  "CONS_def"
skalberg@14516
   134
skalberg@14516
   135
end