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