src/HOL/Import/HOL/rich_list.imp
author skalberg
Fri, 01 Apr 2005 18:59:17 +0200
changeset 15647 b1f486a9c56b
parent 14516 a183dec876ab
child 17188 a26a4fc323ed
permissions -rw-r--r--
Updated import configuration.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     1
import
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     2
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     3
import_segment "hol4"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     4
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     5
def_maps
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     6
  "UNZIP_SND" > "UNZIP_SND_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     7
  "UNZIP_FST" > "UNZIP_FST_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     8
  "SUFFIX" > "SUFFIX_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     9
  "SPLITP" > "SPLITP_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    10
  "SNOC" > "SNOC_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    11
  "SEG" > "SEG_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    12
  "SCANR" > "SCANR_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    13
  "SCANL" > "SCANL_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    14
  "REPLICATE" > "REPLICATE_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    15
  "PREFIX" > "PREFIX_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    16
  "OR_EL" > "OR_EL_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    17
  "LASTN" > "LASTN_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    18
  "IS_SUFFIX" > "IS_SUFFIX_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    19
  "IS_SUBLIST" > "IS_SUBLIST_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    20
  "IS_PREFIX" > "IS_PREFIX_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    21
  "GENLIST" > "GENLIST_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    22
  "FIRSTN" > "FIRSTN_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    23
  "ELL" > "ELL_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    24
  "BUTLASTN" > "BUTLASTN_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    25
  "BUTFIRSTN" > "BUTFIRSTN_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    26
  "AND_EL" > "AND_EL_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    27
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    28
const_maps
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    29
  "UNZIP_SND" > "HOL4Base.rich_list.UNZIP_SND"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    30
  "UNZIP_FST" > "HOL4Base.rich_list.UNZIP_FST"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    31
  "SUFFIX" > "HOL4Base.rich_list.SUFFIX"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    32
  "PREFIX" > "HOL4Base.rich_list.PREFIX"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    33
  "OR_EL" > "HOL4Base.rich_list.OR_EL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    34
  "AND_EL" > "HOL4Base.rich_list.AND_EL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    35
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    36
thm_maps
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    37
  "list_INDUCT" > "HOL4Compat.unzip.induct"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    38
  "list_CASES" > "HOL4Compat.list_CASES"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    39
  "ZIP_UNZIP" > "HOL4Base.list.ZIP_UNZIP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    40
  "ZIP_SNOC" > "HOL4Base.rich_list.ZIP_SNOC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    41
  "ZIP" > "HOL4Compat.ZIP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    42
  "UNZIP_ZIP" > "HOL4Base.list.UNZIP_ZIP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    43
  "UNZIP_SNOC" > "HOL4Base.rich_list.UNZIP_SNOC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    44
  "UNZIP_SND_def" > "HOL4Base.rich_list.UNZIP_SND_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    45
  "UNZIP_SND_DEF" > "HOL4Base.rich_list.UNZIP_SND_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    46
  "UNZIP_FST_def" > "HOL4Base.rich_list.UNZIP_FST_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    47
  "UNZIP_FST_DEF" > "HOL4Base.rich_list.UNZIP_FST_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    48
  "UNZIP" > "HOL4Compat.UNZIP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    49
  "TL_SNOC" > "HOL4Base.rich_list.TL_SNOC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    50
  "TL" > "List.tl.simps_2"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    51
  "SUM_SNOC" > "HOL4Base.rich_list.SUM_SNOC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    52
  "SUM_REVERSE" > "HOL4Base.rich_list.SUM_REVERSE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    53
  "SUM_FOLDR" > "HOL4Compat.sum_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    54
  "SUM_FOLDL" > "HOL4Base.rich_list.SUM_FOLDL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    55
  "SUM_FLAT" > "HOL4Base.rich_list.SUM_FLAT"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    56
  "SUM_APPEND" > "HOL4Base.rich_list.SUM_APPEND"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    57
  "SUM" > "HOL4Compat.SUM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    58
  "SUFFIX_def" > "HOL4Base.rich_list.SUFFIX_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    59
  "SUFFIX_DEF" > "HOL4Base.rich_list.SUFFIX_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    60
  "SPLITP" > "HOL4Base.rich_list.SPLITP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    61
  "SOME_EL_SNOC" > "HOL4Base.rich_list.SOME_EL_SNOC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    62
  "SOME_EL_SEG" > "HOL4Base.rich_list.SOME_EL_SEG"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    63
  "SOME_EL_REVERSE" > "HOL4Base.rich_list.SOME_EL_REVERSE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    64
  "SOME_EL_MAP" > "HOL4Base.rich_list.SOME_EL_MAP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    65
  "SOME_EL_LASTN" > "HOL4Base.rich_list.SOME_EL_LASTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    66
  "SOME_EL_FOLDR_MAP" > "HOL4Base.rich_list.SOME_EL_FOLDR_MAP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    67
  "SOME_EL_FOLDR" > "HOL4Base.rich_list.SOME_EL_FOLDR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    68
  "SOME_EL_FOLDL_MAP" > "HOL4Base.rich_list.SOME_EL_FOLDL_MAP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    69
  "SOME_EL_FOLDL" > "HOL4Base.rich_list.SOME_EL_FOLDL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    70
  "SOME_EL_FIRSTN" > "HOL4Base.rich_list.SOME_EL_FIRSTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    71
  "SOME_EL_DISJ" > "HOL4Base.rich_list.SOME_EL_DISJ"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    72
  "SOME_EL_BUTLASTN" > "HOL4Base.rich_list.SOME_EL_BUTLASTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    73
  "SOME_EL_BUTFIRSTN" > "HOL4Base.rich_list.SOME_EL_BUTFIRSTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    74
  "SOME_EL_APPEND" > "HOL4Base.list.EXISTS_APPEND"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    75
  "SOME_EL" > "HOL4Compat.list_exists_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    76
  "SNOC_REVERSE_CONS" > "HOL4Base.rich_list.SNOC_REVERSE_CONS"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    77
  "SNOC_INDUCT" > "HOL4Base.rich_list.SNOC_INDUCT"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    78
  "SNOC_FOLDR" > "HOL4Base.rich_list.SNOC_FOLDR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    79
  "SNOC_EQ_LENGTH_EQ" > "HOL4Base.rich_list.SNOC_EQ_LENGTH_EQ"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    80
  "SNOC_CASES" > "HOL4Base.rich_list.SNOC_CASES"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    81
  "SNOC_Axiom" > "HOL4Base.rich_list.SNOC_Axiom"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    82
  "SNOC_APPEND" > "HOL4Base.rich_list.SNOC_APPEND"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    83
  "SNOC_11" > "HOL4Base.rich_list.SNOC_11"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    84
  "SNOC" > "HOL4Base.rich_list.SNOC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    85
  "SEG_SUC_CONS" > "HOL4Base.rich_list.SEG_SUC_CONS"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    86
  "SEG_SNOC" > "HOL4Base.rich_list.SEG_SNOC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    87
  "SEG_SEG" > "HOL4Base.rich_list.SEG_SEG"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    88
  "SEG_REVERSE" > "HOL4Base.rich_list.SEG_REVERSE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    89
  "SEG_LENGTH_SNOC" > "HOL4Base.rich_list.SEG_LENGTH_SNOC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    90
  "SEG_LENGTH_ID" > "HOL4Base.rich_list.SEG_LENGTH_ID"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    91
  "SEG_LASTN_BUTLASTN" > "HOL4Base.rich_list.SEG_LASTN_BUTLASTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    92
  "SEG_FIRSTN_BUTFISTN" > "HOL4Base.rich_list.SEG_FIRSTN_BUTFISTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    93
  "SEG_APPEND2" > "HOL4Base.rich_list.SEG_APPEND2"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    94
  "SEG_APPEND1" > "HOL4Base.rich_list.SEG_APPEND1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    95
  "SEG_APPEND" > "HOL4Base.rich_list.SEG_APPEND"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    96
  "SEG_0_SNOC" > "HOL4Base.rich_list.SEG_0_SNOC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    97
  "SEG" > "HOL4Base.rich_list.SEG"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    98
  "SCANR" > "HOL4Base.rich_list.SCANR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    99
  "SCANL" > "HOL4Base.rich_list.SCANL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   100
  "REVERSE_SNOC" > "HOL4Base.rich_list.REVERSE_SNOC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   101
  "REVERSE_REVERSE" > "List.rev_rev_ident"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   102
  "REVERSE_FOLDR" > "HOL4Base.rich_list.REVERSE_FOLDR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   103
  "REVERSE_FOLDL" > "HOL4Base.rich_list.REVERSE_FOLDL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   104
  "REVERSE_FLAT" > "HOL4Base.rich_list.REVERSE_FLAT"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   105
  "REVERSE_EQ_NIL" > "List.rev_is_Nil_conv"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   106
  "REVERSE_APPEND" > "List.rev_append"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   107
  "REVERSE" > "HOL4Base.rich_list.REVERSE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   108
  "REPLICATE" > "HOL4Base.rich_list.REPLICATE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   109
  "PREFIX_def" > "HOL4Base.rich_list.PREFIX_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   110
  "PREFIX_FOLDR" > "HOL4Base.rich_list.PREFIX_FOLDR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   111
  "PREFIX_DEF" > "HOL4Base.rich_list.PREFIX_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   112
  "PREFIX" > "HOL4Base.rich_list.PREFIX"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   113
  "OR_EL_def" > "HOL4Base.rich_list.OR_EL_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   114
  "OR_EL_FOLDR" > "HOL4Base.rich_list.OR_EL_FOLDR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   115
  "OR_EL_FOLDL" > "HOL4Base.rich_list.OR_EL_FOLDL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   116
  "OR_EL_DEF" > "HOL4Base.rich_list.OR_EL_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   117
  "NULL_FOLDR" > "HOL4Base.rich_list.NULL_FOLDR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   118
  "NULL_FOLDL" > "HOL4Base.rich_list.NULL_FOLDL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   119
  "NULL_EQ_NIL" > "HOL4Base.rich_list.NULL_EQ_NIL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   120
  "NULL_DEF" > "HOL4Compat.NULL_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   121
  "NULL" > "HOL4Base.list.NULL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   122
  "NOT_SOME_EL_ALL_EL" > "HOL4Base.list.NOT_EXISTS"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   123
  "NOT_SNOC_NIL" > "HOL4Base.rich_list.NOT_SNOC_NIL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   124
  "NOT_NIL_SNOC" > "HOL4Base.rich_list.NOT_NIL_SNOC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   125
  "NOT_NIL_CONS" > "List.list.simps_1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   126
  "NOT_EQ_LIST" > "HOL4Base.list.NOT_EQ_LIST"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   127
  "NOT_CONS_NIL" > "List.list.simps_2"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   128
  "NOT_ALL_EL_SOME_EL" > "HOL4Base.list.NOT_EVERY"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   129
  "MONOID_APPEND_NIL" > "HOL4Base.rich_list.MONOID_APPEND_NIL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   130
  "MAP_o" > "HOL4Base.rich_list.MAP_o"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   131
  "MAP_SNOC" > "HOL4Base.rich_list.MAP_SNOC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   132
  "MAP_REVERSE" > "List.rev_map"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   133
  "MAP_MAP_o" > "List.map_compose"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   134
  "MAP_FOLDR" > "HOL4Base.rich_list.MAP_FOLDR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   135
  "MAP_FOLDL" > "HOL4Base.rich_list.MAP_FOLDL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   136
  "MAP_FLAT" > "List.map_concat"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   137
  "MAP_FILTER" > "HOL4Base.rich_list.MAP_FILTER"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   138
  "MAP_APPEND" > "List.map_append"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   139
  "MAP2_ZIP" > "HOL4Base.list.MAP2_ZIP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   140
  "MAP2" > "HOL4Compat.MAP2"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   141
  "MAP" > "HOL4Compat.MAP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   142
  "LIST_NOT_EQ" > "HOL4Base.list.LIST_NOT_EQ"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   143
  "LENGTH_ZIP" > "HOL4Base.list.LENGTH_ZIP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   144
  "LENGTH_UNZIP_SND" > "HOL4Base.rich_list.LENGTH_UNZIP_SND"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   145
  "LENGTH_UNZIP_FST" > "HOL4Base.rich_list.LENGTH_UNZIP_FST"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   146
  "LENGTH_SNOC" > "HOL4Base.rich_list.LENGTH_SNOC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   147
  "LENGTH_SEG" > "HOL4Base.rich_list.LENGTH_SEG"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   148
  "LENGTH_SCANR" > "HOL4Base.rich_list.LENGTH_SCANR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   149
  "LENGTH_SCANL" > "HOL4Base.rich_list.LENGTH_SCANL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   150
  "LENGTH_REVERSE" > "List.length_rev"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   151
  "LENGTH_REPLICATE" > "HOL4Base.rich_list.LENGTH_REPLICATE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   152
  "LENGTH_NOT_NULL" > "HOL4Base.rich_list.LENGTH_NOT_NULL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   153
  "LENGTH_NIL" > "List.length_0_conv"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   154
  "LENGTH_MAP2" > "HOL4Base.rich_list.LENGTH_MAP2"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   155
  "LENGTH_MAP" > "List.length_map"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   156
  "LENGTH_LASTN" > "HOL4Base.rich_list.LENGTH_LASTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   157
  "LENGTH_GENLIST" > "HOL4Base.rich_list.LENGTH_GENLIST"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   158
  "LENGTH_FOLDR" > "HOL4Base.rich_list.LENGTH_FOLDR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   159
  "LENGTH_FOLDL" > "HOL4Base.rich_list.LENGTH_FOLDL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   160
  "LENGTH_FLAT" > "HOL4Base.rich_list.LENGTH_FLAT"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   161
  "LENGTH_FIRSTN" > "HOL4Base.rich_list.LENGTH_FIRSTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   162
  "LENGTH_EQ_NIL" > "HOL4Base.list.LENGTH_EQ_NIL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   163
  "LENGTH_EQ" > "HOL4Base.rich_list.LENGTH_EQ"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   164
  "LENGTH_CONS" > "HOL4Base.list.LENGTH_CONS"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   165
  "LENGTH_BUTLASTN" > "HOL4Base.rich_list.LENGTH_BUTLASTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   166
  "LENGTH_BUTLAST" > "HOL4Base.rich_list.LENGTH_BUTLAST"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   167
  "LENGTH_BUTFIRSTN" > "HOL4Base.rich_list.LENGTH_BUTFIRSTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   168
  "LENGTH_APPEND" > "List.length_append"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   169
  "LENGTH" > "HOL4Compat.LENGTH"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   170
  "LAST_LASTN_LAST" > "HOL4Base.rich_list.LAST_LASTN_LAST"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   171
  "LAST_CONS" > "HOL4Base.list.LAST_CONS"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   172
  "LASTN_SEG" > "HOL4Base.rich_list.LASTN_SEG"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   173
  "LASTN_REVERSE" > "HOL4Base.rich_list.LASTN_REVERSE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   174
  "LASTN_MAP" > "HOL4Base.rich_list.LASTN_MAP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   175
  "LASTN_LENGTH_ID" > "HOL4Base.rich_list.LASTN_LENGTH_ID"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   176
  "LASTN_LENGTH_APPEND" > "HOL4Base.rich_list.LASTN_LENGTH_APPEND"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   177
  "LASTN_LASTN" > "HOL4Base.rich_list.LASTN_LASTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   178
  "LASTN_CONS" > "HOL4Base.rich_list.LASTN_CONS"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   179
  "LASTN_BUTLASTN" > "HOL4Base.rich_list.LASTN_BUTLASTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   180
  "LASTN_BUTFIRSTN" > "HOL4Base.rich_list.LASTN_BUTFIRSTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   181
  "LASTN_APPEND2" > "HOL4Base.rich_list.LASTN_APPEND2"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   182
  "LASTN_APPEND1" > "HOL4Base.rich_list.LASTN_APPEND1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   183
  "LASTN_1" > "HOL4Base.rich_list.LASTN_1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   184
  "LASTN" > "HOL4Base.rich_list.LASTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   185
  "LAST" > "HOL4Base.rich_list.LAST"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   186
  "IS_SUFFIX_REVERSE" > "HOL4Base.rich_list.IS_SUFFIX_REVERSE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   187
  "IS_SUFFIX_IS_SUBLIST" > "HOL4Base.rich_list.IS_SUFFIX_IS_SUBLIST"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   188
  "IS_SUFFIX_APPEND" > "HOL4Base.rich_list.IS_SUFFIX_APPEND"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   189
  "IS_SUFFIX" > "HOL4Base.rich_list.IS_SUFFIX"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   190
  "IS_SUBLIST_REVERSE" > "HOL4Base.rich_list.IS_SUBLIST_REVERSE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   191
  "IS_SUBLIST_APPEND" > "HOL4Base.rich_list.IS_SUBLIST_APPEND"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   192
  "IS_SUBLIST" > "HOL4Base.rich_list.IS_SUBLIST"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   193
  "IS_PREFIX_REVERSE" > "HOL4Base.rich_list.IS_PREFIX_REVERSE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   194
  "IS_PREFIX_PREFIX" > "HOL4Base.rich_list.IS_PREFIX_PREFIX"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   195
  "IS_PREFIX_IS_SUBLIST" > "HOL4Base.rich_list.IS_PREFIX_IS_SUBLIST"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   196
  "IS_PREFIX_APPEND" > "HOL4Base.rich_list.IS_PREFIX_APPEND"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   197
  "IS_PREFIX" > "HOL4Base.rich_list.IS_PREFIX"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   198
  "IS_EL_SOME_EL" > "HOL4Base.rich_list.IS_EL_SOME_EL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   199
  "IS_EL_SNOC" > "HOL4Base.rich_list.IS_EL_SNOC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   200
  "IS_EL_SEG" > "HOL4Base.rich_list.IS_EL_SEG"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   201
  "IS_EL_REVERSE" > "HOL4Base.rich_list.IS_EL_REVERSE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   202
  "IS_EL_REPLICATE" > "HOL4Base.rich_list.IS_EL_REPLICATE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   203
  "IS_EL_LASTN" > "HOL4Base.rich_list.IS_EL_LASTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   204
  "IS_EL_FOLDR_MAP" > "HOL4Base.rich_list.IS_EL_FOLDR_MAP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   205
  "IS_EL_FOLDR" > "HOL4Base.rich_list.IS_EL_FOLDR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   206
  "IS_EL_FOLDL_MAP" > "HOL4Base.rich_list.IS_EL_FOLDL_MAP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   207
  "IS_EL_FOLDL" > "HOL4Base.rich_list.IS_EL_FOLDL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   208
  "IS_EL_FIRSTN" > "HOL4Base.rich_list.IS_EL_FIRSTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   209
  "IS_EL_FILTER" > "HOL4Base.rich_list.IS_EL_FILTER"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   210
  "IS_EL_DEF" > "HOL4Base.rich_list.IS_EL_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   211
  "IS_EL_BUTLASTN" > "HOL4Base.rich_list.IS_EL_BUTLASTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   212
  "IS_EL_BUTFIRSTN" > "HOL4Base.rich_list.IS_EL_BUTFIRSTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   213
  "IS_EL_APPEND" > "HOL4Base.list.MEM_APPEND"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   214
  "IS_EL" > "HOL4Compat.MEM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   215
  "HD" > "List.hd.simps"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   216
  "GENLIST" > "HOL4Base.rich_list.GENLIST"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   217
  "FOLDR_SNOC" > "HOL4Base.rich_list.FOLDR_SNOC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   218
  "FOLDR_SINGLE" > "HOL4Base.rich_list.FOLDR_SINGLE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   219
  "FOLDR_REVERSE" > "HOL4Base.rich_list.FOLDR_REVERSE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   220
  "FOLDR_MAP_REVERSE" > "HOL4Base.rich_list.FOLDR_MAP_REVERSE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   221
  "FOLDR_MAP" > "HOL4Base.rich_list.FOLDR_MAP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   222
  "FOLDR_FOLDL_REVERSE" > "List.foldr_foldl"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   223
  "FOLDR_FOLDL" > "HOL4Base.rich_list.FOLDR_FOLDL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   224
  "FOLDR_FILTER_REVERSE" > "HOL4Base.rich_list.FOLDR_FILTER_REVERSE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   225
  "FOLDR_FILTER" > "HOL4Base.rich_list.FOLDR_FILTER"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   226
  "FOLDR_CONS_NIL" > "HOL4Base.rich_list.FOLDR_CONS_NIL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   227
  "FOLDR_APPEND" > "List.foldr_append"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   228
  "FOLDR" > "HOL4Compat.FOLDR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   229
  "FOLDL_SNOC_NIL" > "HOL4Base.rich_list.FOLDL_SNOC_NIL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   230
  "FOLDL_SNOC" > "HOL4Base.rich_list.FOLDL_SNOC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   231
  "FOLDL_SINGLE" > "HOL4Base.rich_list.FOLDL_SINGLE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   232
  "FOLDL_REVERSE" > "HOL4Base.rich_list.FOLDL_REVERSE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   233
  "FOLDL_MAP" > "HOL4Base.rich_list.FOLDL_MAP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   234
  "FOLDL_FOLDR_REVERSE" > "List.foldl_foldr"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   235
  "FOLDL_FILTER" > "HOL4Base.rich_list.FOLDL_FILTER"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   236
  "FOLDL_APPEND" > "List.foldl_append"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   237
  "FOLDL" > "HOL4Compat.FOLDL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   238
  "FLAT_SNOC" > "HOL4Base.rich_list.FLAT_SNOC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   239
  "FLAT_REVERSE" > "HOL4Base.rich_list.FLAT_REVERSE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   240
  "FLAT_FOLDR" > "HOL4Base.rich_list.FLAT_FOLDR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   241
  "FLAT_FOLDL" > "HOL4Base.rich_list.FLAT_FOLDL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   242
  "FLAT_FLAT" > "HOL4Base.rich_list.FLAT_FLAT"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   243
  "FLAT_APPEND" > "List.concat_append"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   244
  "FLAT" > "HOL4Compat.FLAT"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   245
  "FIRSTN_SNOC" > "HOL4Base.rich_list.FIRSTN_SNOC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   246
  "FIRSTN_SEG" > "HOL4Base.rich_list.FIRSTN_SEG"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   247
  "FIRSTN_REVERSE" > "HOL4Base.rich_list.FIRSTN_REVERSE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   248
  "FIRSTN_LENGTH_ID" > "HOL4Base.rich_list.FIRSTN_LENGTH_ID"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   249
  "FIRSTN_LENGTH_APPEND" > "HOL4Base.rich_list.FIRSTN_LENGTH_APPEND"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   250
  "FIRSTN_FIRSTN" > "HOL4Base.rich_list.FIRSTN_FIRSTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   251
  "FIRSTN_BUTLASTN" > "HOL4Base.rich_list.FIRSTN_BUTLASTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   252
  "FIRSTN_APPEND2" > "HOL4Base.rich_list.FIRSTN_APPEND2"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   253
  "FIRSTN_APPEND1" > "HOL4Base.rich_list.FIRSTN_APPEND1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   254
  "FIRSTN" > "HOL4Base.rich_list.FIRSTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   255
  "FILTER_SNOC" > "HOL4Base.rich_list.FILTER_SNOC"
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 14516
diff changeset
   256
  "FILTER_REVERSE" > "List.rev_filter"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   257
  "FILTER_MAP" > "HOL4Base.rich_list.FILTER_MAP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   258
  "FILTER_IDEM" > "HOL4Base.rich_list.FILTER_IDEM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   259
  "FILTER_FOLDR" > "HOL4Base.rich_list.FILTER_FOLDR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   260
  "FILTER_FOLDL" > "HOL4Base.rich_list.FILTER_FOLDL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   261
  "FILTER_FLAT" > "List.filter_concat"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   262
  "FILTER_FILTER" > "HOL4Base.rich_list.FILTER_FILTER"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   263
  "FILTER_COMM" > "HOL4Base.rich_list.FILTER_COMM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   264
  "FILTER_APPEND" > "List.filter_append"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   265
  "FILTER" > "HOL4Compat.FILTER"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   266
  "FCOMM_FOLDR_FLAT" > "HOL4Base.rich_list.FCOMM_FOLDR_FLAT"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   267
  "FCOMM_FOLDR_APPEND" > "HOL4Base.rich_list.FCOMM_FOLDR_APPEND"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   268
  "FCOMM_FOLDL_FLAT" > "HOL4Base.rich_list.FCOMM_FOLDL_FLAT"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   269
  "FCOMM_FOLDL_APPEND" > "HOL4Base.rich_list.FCOMM_FOLDL_APPEND"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   270
  "EQ_LIST" > "HOL4Base.list.EQ_LIST"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   271
  "EL_SNOC" > "HOL4Base.rich_list.EL_SNOC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   272
  "EL_SEG" > "HOL4Base.rich_list.EL_SEG"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   273
  "EL_REVERSE_ELL" > "HOL4Base.rich_list.EL_REVERSE_ELL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   274
  "EL_REVERSE" > "HOL4Base.rich_list.EL_REVERSE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   275
  "EL_PRE_LENGTH" > "HOL4Base.rich_list.EL_PRE_LENGTH"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   276
  "EL_MAP" > "HOL4Base.rich_list.EL_MAP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   277
  "EL_LENGTH_SNOC" > "HOL4Base.rich_list.EL_LENGTH_SNOC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   278
  "EL_LENGTH_APPEND" > "HOL4Base.rich_list.EL_LENGTH_APPEND"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   279
  "EL_IS_EL" > "HOL4Base.rich_list.EL_IS_EL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   280
  "EL_ELL" > "HOL4Base.rich_list.EL_ELL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   281
  "EL_CONS" > "HOL4Base.rich_list.EL_CONS"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   282
  "EL_APPEND2" > "HOL4Base.rich_list.EL_APPEND2"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   283
  "EL_APPEND1" > "HOL4Base.rich_list.EL_APPEND1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   284
  "ELL_SUC_SNOC" > "HOL4Base.rich_list.ELL_SUC_SNOC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   285
  "ELL_SNOC" > "HOL4Base.rich_list.ELL_SNOC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   286
  "ELL_SEG" > "HOL4Base.rich_list.ELL_SEG"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   287
  "ELL_REVERSE_EL" > "HOL4Base.rich_list.ELL_REVERSE_EL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   288
  "ELL_REVERSE" > "HOL4Base.rich_list.ELL_REVERSE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   289
  "ELL_PRE_LENGTH" > "HOL4Base.rich_list.ELL_PRE_LENGTH"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   290
  "ELL_MAP" > "HOL4Base.rich_list.ELL_MAP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   291
  "ELL_LENGTH_SNOC" > "HOL4Base.rich_list.ELL_LENGTH_SNOC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   292
  "ELL_LENGTH_CONS" > "HOL4Base.rich_list.ELL_LENGTH_CONS"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   293
  "ELL_LENGTH_APPEND" > "HOL4Base.rich_list.ELL_LENGTH_APPEND"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   294
  "ELL_LAST" > "HOL4Base.rich_list.ELL_LAST"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   295
  "ELL_IS_EL" > "HOL4Base.rich_list.ELL_IS_EL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   296
  "ELL_EL" > "HOL4Base.rich_list.ELL_EL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   297
  "ELL_CONS" > "HOL4Base.rich_list.ELL_CONS"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   298
  "ELL_APPEND2" > "HOL4Base.rich_list.ELL_APPEND2"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   299
  "ELL_APPEND1" > "HOL4Base.rich_list.ELL_APPEND1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   300
  "ELL_0_SNOC" > "HOL4Base.rich_list.ELL_0_SNOC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   301
  "ELL" > "HOL4Base.rich_list.ELL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   302
  "EL" > "HOL4Base.rich_list.EL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   303
  "CONS_APPEND" > "HOL4Base.rich_list.CONS_APPEND"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   304
  "CONS_11" > "List.list.simps_3"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   305
  "CONS" > "HOL4Base.list.CONS"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   306
  "COMM_MONOID_FOLDR" > "HOL4Base.rich_list.COMM_MONOID_FOLDR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   307
  "COMM_MONOID_FOLDL" > "HOL4Base.rich_list.COMM_MONOID_FOLDL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   308
  "COMM_ASSOC_FOLDR_REVERSE" > "HOL4Base.rich_list.COMM_ASSOC_FOLDR_REVERSE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   309
  "COMM_ASSOC_FOLDL_REVERSE" > "HOL4Base.rich_list.COMM_ASSOC_FOLDL_REVERSE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   310
  "BUTLAST_CONS" > "HOL4Base.list.FRONT_CONS"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   311
  "BUTLASTN_SUC_BUTLAST" > "HOL4Base.rich_list.BUTLASTN_SUC_BUTLAST"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   312
  "BUTLASTN_SEG" > "HOL4Base.rich_list.BUTLASTN_SEG"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   313
  "BUTLASTN_REVERSE" > "HOL4Base.rich_list.BUTLASTN_REVERSE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   314
  "BUTLASTN_MAP" > "HOL4Base.rich_list.BUTLASTN_MAP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   315
  "BUTLASTN_LENGTH_NIL" > "HOL4Base.rich_list.BUTLASTN_LENGTH_NIL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   316
  "BUTLASTN_LENGTH_CONS" > "HOL4Base.rich_list.BUTLASTN_LENGTH_CONS"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   317
  "BUTLASTN_LENGTH_APPEND" > "HOL4Base.rich_list.BUTLASTN_LENGTH_APPEND"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   318
  "BUTLASTN_LASTN_NIL" > "HOL4Base.rich_list.BUTLASTN_LASTN_NIL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   319
  "BUTLASTN_LASTN" > "HOL4Base.rich_list.BUTLASTN_LASTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   320
  "BUTLASTN_FIRSTN" > "HOL4Base.rich_list.BUTLASTN_FIRSTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   321
  "BUTLASTN_CONS" > "HOL4Base.rich_list.BUTLASTN_CONS"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   322
  "BUTLASTN_BUTLASTN" > "HOL4Base.rich_list.BUTLASTN_BUTLASTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   323
  "BUTLASTN_BUTLAST" > "HOL4Base.rich_list.BUTLASTN_BUTLAST"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   324
  "BUTLASTN_APPEND2" > "HOL4Base.rich_list.BUTLASTN_APPEND2"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   325
  "BUTLASTN_APPEND1" > "HOL4Base.rich_list.BUTLASTN_APPEND1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   326
  "BUTLASTN_1" > "HOL4Base.rich_list.BUTLASTN_1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   327
  "BUTLASTN" > "HOL4Base.rich_list.BUTLASTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   328
  "BUTLAST" > "HOL4Base.rich_list.BUTLAST"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   329
  "BUTFIRSTN_SNOC" > "HOL4Base.rich_list.BUTFIRSTN_SNOC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   330
  "BUTFIRSTN_SEG" > "HOL4Base.rich_list.BUTFIRSTN_SEG"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   331
  "BUTFIRSTN_REVERSE" > "HOL4Base.rich_list.BUTFIRSTN_REVERSE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   332
  "BUTFIRSTN_LENGTH_NIL" > "HOL4Base.rich_list.BUTFIRSTN_LENGTH_NIL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   333
  "BUTFIRSTN_LENGTH_APPEND" > "HOL4Base.rich_list.BUTFIRSTN_LENGTH_APPEND"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   334
  "BUTFIRSTN_LASTN" > "HOL4Base.rich_list.BUTFIRSTN_LASTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   335
  "BUTFIRSTN_BUTFIRSTN" > "HOL4Base.rich_list.BUTFIRSTN_BUTFIRSTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   336
  "BUTFIRSTN_APPEND2" > "HOL4Base.rich_list.BUTFIRSTN_APPEND2"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   337
  "BUTFIRSTN_APPEND1" > "HOL4Base.rich_list.BUTFIRSTN_APPEND1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   338
  "BUTFIRSTN" > "HOL4Base.rich_list.BUTFIRSTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   339
  "ASSOC_FOLDR_FLAT" > "HOL4Base.rich_list.ASSOC_FOLDR_FLAT"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   340
  "ASSOC_FOLDL_FLAT" > "HOL4Base.rich_list.ASSOC_FOLDL_FLAT"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   341
  "ASSOC_APPEND" > "HOL4Base.rich_list.ASSOC_APPEND"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   342
  "APPEND_SNOC" > "HOL4Base.rich_list.APPEND_SNOC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   343
  "APPEND_NIL" > "HOL4Base.rich_list.APPEND_NIL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   344
  "APPEND_LENGTH_EQ" > "HOL4Base.rich_list.APPEND_LENGTH_EQ"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   345
  "APPEND_FOLDR" > "HOL4Base.rich_list.APPEND_FOLDR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   346
  "APPEND_FOLDL" > "HOL4Base.rich_list.APPEND_FOLDL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   347
  "APPEND_FIRSTN_LASTN" > "HOL4Base.rich_list.APPEND_FIRSTN_LASTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   348
  "APPEND_FIRSTN_BUTFIRSTN" > "HOL4Base.rich_list.APPEND_FIRSTN_BUTFIRSTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   349
  "APPEND_BUTLAST_LAST" > "List.append_butlast_last_id"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   350
  "APPEND_BUTLASTN_LASTN" > "HOL4Base.rich_list.APPEND_BUTLASTN_LASTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   351
  "APPEND_BUTLASTN_BUTFIRSTN" > "HOL4Base.rich_list.APPEND_BUTLASTN_BUTFIRSTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   352
  "APPEND_ASSOC" > "List.append_assoc"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   353
  "APPEND" > "HOL4Compat.APPEND"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   354
  "AND_EL_def" > "HOL4Base.rich_list.AND_EL_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   355
  "AND_EL_FOLDR" > "HOL4Base.rich_list.AND_EL_FOLDR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   356
  "AND_EL_FOLDL" > "HOL4Base.rich_list.AND_EL_FOLDL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   357
  "AND_EL_DEF" > "HOL4Base.rich_list.AND_EL_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   358
  "ALL_EL_SNOC" > "HOL4Base.rich_list.ALL_EL_SNOC"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   359
  "ALL_EL_SEG" > "HOL4Base.rich_list.ALL_EL_SEG"
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 14516
diff changeset
   360
  "ALL_EL_REVERSE" > "List.list_all_rev"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   361
  "ALL_EL_REPLICATE" > "HOL4Base.rich_list.ALL_EL_REPLICATE"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   362
  "ALL_EL_MAP" > "HOL4Base.rich_list.ALL_EL_MAP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   363
  "ALL_EL_LASTN" > "HOL4Base.rich_list.ALL_EL_LASTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   364
  "ALL_EL_FOLDR_MAP" > "HOL4Base.rich_list.ALL_EL_FOLDR_MAP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   365
  "ALL_EL_FOLDR" > "HOL4Base.rich_list.ALL_EL_FOLDR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   366
  "ALL_EL_FOLDL_MAP" > "HOL4Base.rich_list.ALL_EL_FOLDL_MAP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   367
  "ALL_EL_FOLDL" > "HOL4Base.rich_list.ALL_EL_FOLDL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   368
  "ALL_EL_FIRSTN" > "HOL4Base.rich_list.ALL_EL_FIRSTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   369
  "ALL_EL_CONJ" > "HOL4Base.list.EVERY_CONJ"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   370
  "ALL_EL_BUTLASTN" > "HOL4Base.rich_list.ALL_EL_BUTLASTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   371
  "ALL_EL_BUTFIRSTN" > "HOL4Base.rich_list.ALL_EL_BUTFIRSTN"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   372
  "ALL_EL_APPEND" > "List.list_all_append"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   373
  "ALL_EL" > "HOL4Compat.EVERY_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   374
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   375
end