--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/HOL/rich_list.imp Fri Apr 02 17:37:45 2004 +0200
@@ -0,0 +1,375 @@
+import
+
+import_segment "hol4"
+
+def_maps
+ "UNZIP_SND" > "UNZIP_SND_def"
+ "UNZIP_FST" > "UNZIP_FST_def"
+ "SUFFIX" > "SUFFIX_def"
+ "SPLITP" > "SPLITP_def"
+ "SNOC" > "SNOC_def"
+ "SEG" > "SEG_def"
+ "SCANR" > "SCANR_def"
+ "SCANL" > "SCANL_def"
+ "REPLICATE" > "REPLICATE_def"
+ "PREFIX" > "PREFIX_def"
+ "OR_EL" > "OR_EL_def"
+ "LASTN" > "LASTN_def"
+ "IS_SUFFIX" > "IS_SUFFIX_def"
+ "IS_SUBLIST" > "IS_SUBLIST_def"
+ "IS_PREFIX" > "IS_PREFIX_def"
+ "GENLIST" > "GENLIST_def"
+ "FIRSTN" > "FIRSTN_def"
+ "ELL" > "ELL_def"
+ "BUTLASTN" > "BUTLASTN_def"
+ "BUTFIRSTN" > "BUTFIRSTN_def"
+ "AND_EL" > "AND_EL_def"
+
+const_maps
+ "UNZIP_SND" > "HOL4Base.rich_list.UNZIP_SND"
+ "UNZIP_FST" > "HOL4Base.rich_list.UNZIP_FST"
+ "SUFFIX" > "HOL4Base.rich_list.SUFFIX"
+ "PREFIX" > "HOL4Base.rich_list.PREFIX"
+ "OR_EL" > "HOL4Base.rich_list.OR_EL"
+ "AND_EL" > "HOL4Base.rich_list.AND_EL"
+
+thm_maps
+ "list_INDUCT" > "HOL4Compat.unzip.induct"
+ "list_CASES" > "HOL4Compat.list_CASES"
+ "ZIP_UNZIP" > "HOL4Base.list.ZIP_UNZIP"
+ "ZIP_SNOC" > "HOL4Base.rich_list.ZIP_SNOC"
+ "ZIP" > "HOL4Compat.ZIP"
+ "UNZIP_ZIP" > "HOL4Base.list.UNZIP_ZIP"
+ "UNZIP_SNOC" > "HOL4Base.rich_list.UNZIP_SNOC"
+ "UNZIP_SND_def" > "HOL4Base.rich_list.UNZIP_SND_def"
+ "UNZIP_SND_DEF" > "HOL4Base.rich_list.UNZIP_SND_DEF"
+ "UNZIP_FST_def" > "HOL4Base.rich_list.UNZIP_FST_def"
+ "UNZIP_FST_DEF" > "HOL4Base.rich_list.UNZIP_FST_DEF"
+ "UNZIP" > "HOL4Compat.UNZIP"
+ "TL_SNOC" > "HOL4Base.rich_list.TL_SNOC"
+ "TL" > "List.tl.simps_2"
+ "SUM_SNOC" > "HOL4Base.rich_list.SUM_SNOC"
+ "SUM_REVERSE" > "HOL4Base.rich_list.SUM_REVERSE"
+ "SUM_FOLDR" > "HOL4Compat.sum_def"
+ "SUM_FOLDL" > "HOL4Base.rich_list.SUM_FOLDL"
+ "SUM_FLAT" > "HOL4Base.rich_list.SUM_FLAT"
+ "SUM_APPEND" > "HOL4Base.rich_list.SUM_APPEND"
+ "SUM" > "HOL4Compat.SUM"
+ "SUFFIX_def" > "HOL4Base.rich_list.SUFFIX_def"
+ "SUFFIX_DEF" > "HOL4Base.rich_list.SUFFIX_DEF"
+ "SPLITP" > "HOL4Base.rich_list.SPLITP"
+ "SOME_EL_SNOC" > "HOL4Base.rich_list.SOME_EL_SNOC"
+ "SOME_EL_SEG" > "HOL4Base.rich_list.SOME_EL_SEG"
+ "SOME_EL_REVERSE" > "HOL4Base.rich_list.SOME_EL_REVERSE"
+ "SOME_EL_MAP" > "HOL4Base.rich_list.SOME_EL_MAP"
+ "SOME_EL_LASTN" > "HOL4Base.rich_list.SOME_EL_LASTN"
+ "SOME_EL_FOLDR_MAP" > "HOL4Base.rich_list.SOME_EL_FOLDR_MAP"
+ "SOME_EL_FOLDR" > "HOL4Base.rich_list.SOME_EL_FOLDR"
+ "SOME_EL_FOLDL_MAP" > "HOL4Base.rich_list.SOME_EL_FOLDL_MAP"
+ "SOME_EL_FOLDL" > "HOL4Base.rich_list.SOME_EL_FOLDL"
+ "SOME_EL_FIRSTN" > "HOL4Base.rich_list.SOME_EL_FIRSTN"
+ "SOME_EL_DISJ" > "HOL4Base.rich_list.SOME_EL_DISJ"
+ "SOME_EL_BUTLASTN" > "HOL4Base.rich_list.SOME_EL_BUTLASTN"
+ "SOME_EL_BUTFIRSTN" > "HOL4Base.rich_list.SOME_EL_BUTFIRSTN"
+ "SOME_EL_APPEND" > "HOL4Base.list.EXISTS_APPEND"
+ "SOME_EL" > "HOL4Compat.list_exists_DEF"
+ "SNOC_REVERSE_CONS" > "HOL4Base.rich_list.SNOC_REVERSE_CONS"
+ "SNOC_INDUCT" > "HOL4Base.rich_list.SNOC_INDUCT"
+ "SNOC_FOLDR" > "HOL4Base.rich_list.SNOC_FOLDR"
+ "SNOC_EQ_LENGTH_EQ" > "HOL4Base.rich_list.SNOC_EQ_LENGTH_EQ"
+ "SNOC_CASES" > "HOL4Base.rich_list.SNOC_CASES"
+ "SNOC_Axiom" > "HOL4Base.rich_list.SNOC_Axiom"
+ "SNOC_APPEND" > "HOL4Base.rich_list.SNOC_APPEND"
+ "SNOC_11" > "HOL4Base.rich_list.SNOC_11"
+ "SNOC" > "HOL4Base.rich_list.SNOC"
+ "SEG_SUC_CONS" > "HOL4Base.rich_list.SEG_SUC_CONS"
+ "SEG_SNOC" > "HOL4Base.rich_list.SEG_SNOC"
+ "SEG_SEG" > "HOL4Base.rich_list.SEG_SEG"
+ "SEG_REVERSE" > "HOL4Base.rich_list.SEG_REVERSE"
+ "SEG_LENGTH_SNOC" > "HOL4Base.rich_list.SEG_LENGTH_SNOC"
+ "SEG_LENGTH_ID" > "HOL4Base.rich_list.SEG_LENGTH_ID"
+ "SEG_LASTN_BUTLASTN" > "HOL4Base.rich_list.SEG_LASTN_BUTLASTN"
+ "SEG_FIRSTN_BUTFISTN" > "HOL4Base.rich_list.SEG_FIRSTN_BUTFISTN"
+ "SEG_APPEND2" > "HOL4Base.rich_list.SEG_APPEND2"
+ "SEG_APPEND1" > "HOL4Base.rich_list.SEG_APPEND1"
+ "SEG_APPEND" > "HOL4Base.rich_list.SEG_APPEND"
+ "SEG_0_SNOC" > "HOL4Base.rich_list.SEG_0_SNOC"
+ "SEG" > "HOL4Base.rich_list.SEG"
+ "SCANR" > "HOL4Base.rich_list.SCANR"
+ "SCANL" > "HOL4Base.rich_list.SCANL"
+ "REVERSE_SNOC" > "HOL4Base.rich_list.REVERSE_SNOC"
+ "REVERSE_REVERSE" > "List.rev_rev_ident"
+ "REVERSE_FOLDR" > "HOL4Base.rich_list.REVERSE_FOLDR"
+ "REVERSE_FOLDL" > "HOL4Base.rich_list.REVERSE_FOLDL"
+ "REVERSE_FLAT" > "HOL4Base.rich_list.REVERSE_FLAT"
+ "REVERSE_EQ_NIL" > "List.rev_is_Nil_conv"
+ "REVERSE_APPEND" > "List.rev_append"
+ "REVERSE" > "HOL4Base.rich_list.REVERSE"
+ "REPLICATE" > "HOL4Base.rich_list.REPLICATE"
+ "PREFIX_def" > "HOL4Base.rich_list.PREFIX_def"
+ "PREFIX_FOLDR" > "HOL4Base.rich_list.PREFIX_FOLDR"
+ "PREFIX_DEF" > "HOL4Base.rich_list.PREFIX_DEF"
+ "PREFIX" > "HOL4Base.rich_list.PREFIX"
+ "OR_EL_def" > "HOL4Base.rich_list.OR_EL_def"
+ "OR_EL_FOLDR" > "HOL4Base.rich_list.OR_EL_FOLDR"
+ "OR_EL_FOLDL" > "HOL4Base.rich_list.OR_EL_FOLDL"
+ "OR_EL_DEF" > "HOL4Base.rich_list.OR_EL_DEF"
+ "NULL_FOLDR" > "HOL4Base.rich_list.NULL_FOLDR"
+ "NULL_FOLDL" > "HOL4Base.rich_list.NULL_FOLDL"
+ "NULL_EQ_NIL" > "HOL4Base.rich_list.NULL_EQ_NIL"
+ "NULL_DEF" > "HOL4Compat.NULL_DEF"
+ "NULL" > "HOL4Base.list.NULL"
+ "NOT_SOME_EL_ALL_EL" > "HOL4Base.list.NOT_EXISTS"
+ "NOT_SNOC_NIL" > "HOL4Base.rich_list.NOT_SNOC_NIL"
+ "NOT_NIL_SNOC" > "HOL4Base.rich_list.NOT_NIL_SNOC"
+ "NOT_NIL_CONS" > "List.list.simps_1"
+ "NOT_EQ_LIST" > "HOL4Base.list.NOT_EQ_LIST"
+ "NOT_CONS_NIL" > "List.list.simps_2"
+ "NOT_ALL_EL_SOME_EL" > "HOL4Base.list.NOT_EVERY"
+ "MONOID_APPEND_NIL" > "HOL4Base.rich_list.MONOID_APPEND_NIL"
+ "MAP_o" > "HOL4Base.rich_list.MAP_o"
+ "MAP_SNOC" > "HOL4Base.rich_list.MAP_SNOC"
+ "MAP_REVERSE" > "List.rev_map"
+ "MAP_MAP_o" > "List.map_compose"
+ "MAP_FOLDR" > "HOL4Base.rich_list.MAP_FOLDR"
+ "MAP_FOLDL" > "HOL4Base.rich_list.MAP_FOLDL"
+ "MAP_FLAT" > "List.map_concat"
+ "MAP_FILTER" > "HOL4Base.rich_list.MAP_FILTER"
+ "MAP_APPEND" > "List.map_append"
+ "MAP2_ZIP" > "HOL4Base.list.MAP2_ZIP"
+ "MAP2" > "HOL4Compat.MAP2"
+ "MAP" > "HOL4Compat.MAP"
+ "LIST_NOT_EQ" > "HOL4Base.list.LIST_NOT_EQ"
+ "LENGTH_ZIP" > "HOL4Base.list.LENGTH_ZIP"
+ "LENGTH_UNZIP_SND" > "HOL4Base.rich_list.LENGTH_UNZIP_SND"
+ "LENGTH_UNZIP_FST" > "HOL4Base.rich_list.LENGTH_UNZIP_FST"
+ "LENGTH_SNOC" > "HOL4Base.rich_list.LENGTH_SNOC"
+ "LENGTH_SEG" > "HOL4Base.rich_list.LENGTH_SEG"
+ "LENGTH_SCANR" > "HOL4Base.rich_list.LENGTH_SCANR"
+ "LENGTH_SCANL" > "HOL4Base.rich_list.LENGTH_SCANL"
+ "LENGTH_REVERSE" > "List.length_rev"
+ "LENGTH_REPLICATE" > "HOL4Base.rich_list.LENGTH_REPLICATE"
+ "LENGTH_NOT_NULL" > "HOL4Base.rich_list.LENGTH_NOT_NULL"
+ "LENGTH_NIL" > "List.length_0_conv"
+ "LENGTH_MAP2" > "HOL4Base.rich_list.LENGTH_MAP2"
+ "LENGTH_MAP" > "List.length_map"
+ "LENGTH_LASTN" > "HOL4Base.rich_list.LENGTH_LASTN"
+ "LENGTH_GENLIST" > "HOL4Base.rich_list.LENGTH_GENLIST"
+ "LENGTH_FOLDR" > "HOL4Base.rich_list.LENGTH_FOLDR"
+ "LENGTH_FOLDL" > "HOL4Base.rich_list.LENGTH_FOLDL"
+ "LENGTH_FLAT" > "HOL4Base.rich_list.LENGTH_FLAT"
+ "LENGTH_FIRSTN" > "HOL4Base.rich_list.LENGTH_FIRSTN"
+ "LENGTH_EQ_NIL" > "HOL4Base.list.LENGTH_EQ_NIL"
+ "LENGTH_EQ" > "HOL4Base.rich_list.LENGTH_EQ"
+ "LENGTH_CONS" > "HOL4Base.list.LENGTH_CONS"
+ "LENGTH_BUTLASTN" > "HOL4Base.rich_list.LENGTH_BUTLASTN"
+ "LENGTH_BUTLAST" > "HOL4Base.rich_list.LENGTH_BUTLAST"
+ "LENGTH_BUTFIRSTN" > "HOL4Base.rich_list.LENGTH_BUTFIRSTN"
+ "LENGTH_APPEND" > "List.length_append"
+ "LENGTH" > "HOL4Compat.LENGTH"
+ "LAST_LASTN_LAST" > "HOL4Base.rich_list.LAST_LASTN_LAST"
+ "LAST_CONS" > "HOL4Base.list.LAST_CONS"
+ "LASTN_SEG" > "HOL4Base.rich_list.LASTN_SEG"
+ "LASTN_REVERSE" > "HOL4Base.rich_list.LASTN_REVERSE"
+ "LASTN_MAP" > "HOL4Base.rich_list.LASTN_MAP"
+ "LASTN_LENGTH_ID" > "HOL4Base.rich_list.LASTN_LENGTH_ID"
+ "LASTN_LENGTH_APPEND" > "HOL4Base.rich_list.LASTN_LENGTH_APPEND"
+ "LASTN_LASTN" > "HOL4Base.rich_list.LASTN_LASTN"
+ "LASTN_CONS" > "HOL4Base.rich_list.LASTN_CONS"
+ "LASTN_BUTLASTN" > "HOL4Base.rich_list.LASTN_BUTLASTN"
+ "LASTN_BUTFIRSTN" > "HOL4Base.rich_list.LASTN_BUTFIRSTN"
+ "LASTN_APPEND2" > "HOL4Base.rich_list.LASTN_APPEND2"
+ "LASTN_APPEND1" > "HOL4Base.rich_list.LASTN_APPEND1"
+ "LASTN_1" > "HOL4Base.rich_list.LASTN_1"
+ "LASTN" > "HOL4Base.rich_list.LASTN"
+ "LAST" > "HOL4Base.rich_list.LAST"
+ "IS_SUFFIX_REVERSE" > "HOL4Base.rich_list.IS_SUFFIX_REVERSE"
+ "IS_SUFFIX_IS_SUBLIST" > "HOL4Base.rich_list.IS_SUFFIX_IS_SUBLIST"
+ "IS_SUFFIX_APPEND" > "HOL4Base.rich_list.IS_SUFFIX_APPEND"
+ "IS_SUFFIX" > "HOL4Base.rich_list.IS_SUFFIX"
+ "IS_SUBLIST_REVERSE" > "HOL4Base.rich_list.IS_SUBLIST_REVERSE"
+ "IS_SUBLIST_APPEND" > "HOL4Base.rich_list.IS_SUBLIST_APPEND"
+ "IS_SUBLIST" > "HOL4Base.rich_list.IS_SUBLIST"
+ "IS_PREFIX_REVERSE" > "HOL4Base.rich_list.IS_PREFIX_REVERSE"
+ "IS_PREFIX_PREFIX" > "HOL4Base.rich_list.IS_PREFIX_PREFIX"
+ "IS_PREFIX_IS_SUBLIST" > "HOL4Base.rich_list.IS_PREFIX_IS_SUBLIST"
+ "IS_PREFIX_APPEND" > "HOL4Base.rich_list.IS_PREFIX_APPEND"
+ "IS_PREFIX" > "HOL4Base.rich_list.IS_PREFIX"
+ "IS_EL_SOME_EL" > "HOL4Base.rich_list.IS_EL_SOME_EL"
+ "IS_EL_SNOC" > "HOL4Base.rich_list.IS_EL_SNOC"
+ "IS_EL_SEG" > "HOL4Base.rich_list.IS_EL_SEG"
+ "IS_EL_REVERSE" > "HOL4Base.rich_list.IS_EL_REVERSE"
+ "IS_EL_REPLICATE" > "HOL4Base.rich_list.IS_EL_REPLICATE"
+ "IS_EL_LASTN" > "HOL4Base.rich_list.IS_EL_LASTN"
+ "IS_EL_FOLDR_MAP" > "HOL4Base.rich_list.IS_EL_FOLDR_MAP"
+ "IS_EL_FOLDR" > "HOL4Base.rich_list.IS_EL_FOLDR"
+ "IS_EL_FOLDL_MAP" > "HOL4Base.rich_list.IS_EL_FOLDL_MAP"
+ "IS_EL_FOLDL" > "HOL4Base.rich_list.IS_EL_FOLDL"
+ "IS_EL_FIRSTN" > "HOL4Base.rich_list.IS_EL_FIRSTN"
+ "IS_EL_FILTER" > "HOL4Base.rich_list.IS_EL_FILTER"
+ "IS_EL_DEF" > "HOL4Base.rich_list.IS_EL_DEF"
+ "IS_EL_BUTLASTN" > "HOL4Base.rich_list.IS_EL_BUTLASTN"
+ "IS_EL_BUTFIRSTN" > "HOL4Base.rich_list.IS_EL_BUTFIRSTN"
+ "IS_EL_APPEND" > "HOL4Base.list.MEM_APPEND"
+ "IS_EL" > "HOL4Compat.MEM"
+ "HD" > "List.hd.simps"
+ "GENLIST" > "HOL4Base.rich_list.GENLIST"
+ "FOLDR_SNOC" > "HOL4Base.rich_list.FOLDR_SNOC"
+ "FOLDR_SINGLE" > "HOL4Base.rich_list.FOLDR_SINGLE"
+ "FOLDR_REVERSE" > "HOL4Base.rich_list.FOLDR_REVERSE"
+ "FOLDR_MAP_REVERSE" > "HOL4Base.rich_list.FOLDR_MAP_REVERSE"
+ "FOLDR_MAP" > "HOL4Base.rich_list.FOLDR_MAP"
+ "FOLDR_FOLDL_REVERSE" > "List.foldr_foldl"
+ "FOLDR_FOLDL" > "HOL4Base.rich_list.FOLDR_FOLDL"
+ "FOLDR_FILTER_REVERSE" > "HOL4Base.rich_list.FOLDR_FILTER_REVERSE"
+ "FOLDR_FILTER" > "HOL4Base.rich_list.FOLDR_FILTER"
+ "FOLDR_CONS_NIL" > "HOL4Base.rich_list.FOLDR_CONS_NIL"
+ "FOLDR_APPEND" > "List.foldr_append"
+ "FOLDR" > "HOL4Compat.FOLDR"
+ "FOLDL_SNOC_NIL" > "HOL4Base.rich_list.FOLDL_SNOC_NIL"
+ "FOLDL_SNOC" > "HOL4Base.rich_list.FOLDL_SNOC"
+ "FOLDL_SINGLE" > "HOL4Base.rich_list.FOLDL_SINGLE"
+ "FOLDL_REVERSE" > "HOL4Base.rich_list.FOLDL_REVERSE"
+ "FOLDL_MAP" > "HOL4Base.rich_list.FOLDL_MAP"
+ "FOLDL_FOLDR_REVERSE" > "List.foldl_foldr"
+ "FOLDL_FILTER" > "HOL4Base.rich_list.FOLDL_FILTER"
+ "FOLDL_APPEND" > "List.foldl_append"
+ "FOLDL" > "HOL4Compat.FOLDL"
+ "FLAT_SNOC" > "HOL4Base.rich_list.FLAT_SNOC"
+ "FLAT_REVERSE" > "HOL4Base.rich_list.FLAT_REVERSE"
+ "FLAT_FOLDR" > "HOL4Base.rich_list.FLAT_FOLDR"
+ "FLAT_FOLDL" > "HOL4Base.rich_list.FLAT_FOLDL"
+ "FLAT_FLAT" > "HOL4Base.rich_list.FLAT_FLAT"
+ "FLAT_APPEND" > "List.concat_append"
+ "FLAT" > "HOL4Compat.FLAT"
+ "FIRSTN_SNOC" > "HOL4Base.rich_list.FIRSTN_SNOC"
+ "FIRSTN_SEG" > "HOL4Base.rich_list.FIRSTN_SEG"
+ "FIRSTN_REVERSE" > "HOL4Base.rich_list.FIRSTN_REVERSE"
+ "FIRSTN_LENGTH_ID" > "HOL4Base.rich_list.FIRSTN_LENGTH_ID"
+ "FIRSTN_LENGTH_APPEND" > "HOL4Base.rich_list.FIRSTN_LENGTH_APPEND"
+ "FIRSTN_FIRSTN" > "HOL4Base.rich_list.FIRSTN_FIRSTN"
+ "FIRSTN_BUTLASTN" > "HOL4Base.rich_list.FIRSTN_BUTLASTN"
+ "FIRSTN_APPEND2" > "HOL4Base.rich_list.FIRSTN_APPEND2"
+ "FIRSTN_APPEND1" > "HOL4Base.rich_list.FIRSTN_APPEND1"
+ "FIRSTN" > "HOL4Base.rich_list.FIRSTN"
+ "FILTER_SNOC" > "HOL4Base.rich_list.FILTER_SNOC"
+ "FILTER_REVERSE" > "HOL4Base.rich_list.FILTER_REVERSE"
+ "FILTER_MAP" > "HOL4Base.rich_list.FILTER_MAP"
+ "FILTER_IDEM" > "HOL4Base.rich_list.FILTER_IDEM"
+ "FILTER_FOLDR" > "HOL4Base.rich_list.FILTER_FOLDR"
+ "FILTER_FOLDL" > "HOL4Base.rich_list.FILTER_FOLDL"
+ "FILTER_FLAT" > "List.filter_concat"
+ "FILTER_FILTER" > "HOL4Base.rich_list.FILTER_FILTER"
+ "FILTER_COMM" > "HOL4Base.rich_list.FILTER_COMM"
+ "FILTER_APPEND" > "List.filter_append"
+ "FILTER" > "HOL4Compat.FILTER"
+ "FCOMM_FOLDR_FLAT" > "HOL4Base.rich_list.FCOMM_FOLDR_FLAT"
+ "FCOMM_FOLDR_APPEND" > "HOL4Base.rich_list.FCOMM_FOLDR_APPEND"
+ "FCOMM_FOLDL_FLAT" > "HOL4Base.rich_list.FCOMM_FOLDL_FLAT"
+ "FCOMM_FOLDL_APPEND" > "HOL4Base.rich_list.FCOMM_FOLDL_APPEND"
+ "EQ_LIST" > "HOL4Base.list.EQ_LIST"
+ "EL_SNOC" > "HOL4Base.rich_list.EL_SNOC"
+ "EL_SEG" > "HOL4Base.rich_list.EL_SEG"
+ "EL_REVERSE_ELL" > "HOL4Base.rich_list.EL_REVERSE_ELL"
+ "EL_REVERSE" > "HOL4Base.rich_list.EL_REVERSE"
+ "EL_PRE_LENGTH" > "HOL4Base.rich_list.EL_PRE_LENGTH"
+ "EL_MAP" > "HOL4Base.rich_list.EL_MAP"
+ "EL_LENGTH_SNOC" > "HOL4Base.rich_list.EL_LENGTH_SNOC"
+ "EL_LENGTH_APPEND" > "HOL4Base.rich_list.EL_LENGTH_APPEND"
+ "EL_IS_EL" > "HOL4Base.rich_list.EL_IS_EL"
+ "EL_ELL" > "HOL4Base.rich_list.EL_ELL"
+ "EL_CONS" > "HOL4Base.rich_list.EL_CONS"
+ "EL_APPEND2" > "HOL4Base.rich_list.EL_APPEND2"
+ "EL_APPEND1" > "HOL4Base.rich_list.EL_APPEND1"
+ "ELL_SUC_SNOC" > "HOL4Base.rich_list.ELL_SUC_SNOC"
+ "ELL_SNOC" > "HOL4Base.rich_list.ELL_SNOC"
+ "ELL_SEG" > "HOL4Base.rich_list.ELL_SEG"
+ "ELL_REVERSE_EL" > "HOL4Base.rich_list.ELL_REVERSE_EL"
+ "ELL_REVERSE" > "HOL4Base.rich_list.ELL_REVERSE"
+ "ELL_PRE_LENGTH" > "HOL4Base.rich_list.ELL_PRE_LENGTH"
+ "ELL_MAP" > "HOL4Base.rich_list.ELL_MAP"
+ "ELL_LENGTH_SNOC" > "HOL4Base.rich_list.ELL_LENGTH_SNOC"
+ "ELL_LENGTH_CONS" > "HOL4Base.rich_list.ELL_LENGTH_CONS"
+ "ELL_LENGTH_APPEND" > "HOL4Base.rich_list.ELL_LENGTH_APPEND"
+ "ELL_LAST" > "HOL4Base.rich_list.ELL_LAST"
+ "ELL_IS_EL" > "HOL4Base.rich_list.ELL_IS_EL"
+ "ELL_EL" > "HOL4Base.rich_list.ELL_EL"
+ "ELL_CONS" > "HOL4Base.rich_list.ELL_CONS"
+ "ELL_APPEND2" > "HOL4Base.rich_list.ELL_APPEND2"
+ "ELL_APPEND1" > "HOL4Base.rich_list.ELL_APPEND1"
+ "ELL_0_SNOC" > "HOL4Base.rich_list.ELL_0_SNOC"
+ "ELL" > "HOL4Base.rich_list.ELL"
+ "EL" > "HOL4Base.rich_list.EL"
+ "CONS_APPEND" > "HOL4Base.rich_list.CONS_APPEND"
+ "CONS_11" > "List.list.simps_3"
+ "CONS" > "HOL4Base.list.CONS"
+ "COMM_MONOID_FOLDR" > "HOL4Base.rich_list.COMM_MONOID_FOLDR"
+ "COMM_MONOID_FOLDL" > "HOL4Base.rich_list.COMM_MONOID_FOLDL"
+ "COMM_ASSOC_FOLDR_REVERSE" > "HOL4Base.rich_list.COMM_ASSOC_FOLDR_REVERSE"
+ "COMM_ASSOC_FOLDL_REVERSE" > "HOL4Base.rich_list.COMM_ASSOC_FOLDL_REVERSE"
+ "BUTLAST_CONS" > "HOL4Base.list.FRONT_CONS"
+ "BUTLASTN_SUC_BUTLAST" > "HOL4Base.rich_list.BUTLASTN_SUC_BUTLAST"
+ "BUTLASTN_SEG" > "HOL4Base.rich_list.BUTLASTN_SEG"
+ "BUTLASTN_REVERSE" > "HOL4Base.rich_list.BUTLASTN_REVERSE"
+ "BUTLASTN_MAP" > "HOL4Base.rich_list.BUTLASTN_MAP"
+ "BUTLASTN_LENGTH_NIL" > "HOL4Base.rich_list.BUTLASTN_LENGTH_NIL"
+ "BUTLASTN_LENGTH_CONS" > "HOL4Base.rich_list.BUTLASTN_LENGTH_CONS"
+ "BUTLASTN_LENGTH_APPEND" > "HOL4Base.rich_list.BUTLASTN_LENGTH_APPEND"
+ "BUTLASTN_LASTN_NIL" > "HOL4Base.rich_list.BUTLASTN_LASTN_NIL"
+ "BUTLASTN_LASTN" > "HOL4Base.rich_list.BUTLASTN_LASTN"
+ "BUTLASTN_FIRSTN" > "HOL4Base.rich_list.BUTLASTN_FIRSTN"
+ "BUTLASTN_CONS" > "HOL4Base.rich_list.BUTLASTN_CONS"
+ "BUTLASTN_BUTLASTN" > "HOL4Base.rich_list.BUTLASTN_BUTLASTN"
+ "BUTLASTN_BUTLAST" > "HOL4Base.rich_list.BUTLASTN_BUTLAST"
+ "BUTLASTN_APPEND2" > "HOL4Base.rich_list.BUTLASTN_APPEND2"
+ "BUTLASTN_APPEND1" > "HOL4Base.rich_list.BUTLASTN_APPEND1"
+ "BUTLASTN_1" > "HOL4Base.rich_list.BUTLASTN_1"
+ "BUTLASTN" > "HOL4Base.rich_list.BUTLASTN"
+ "BUTLAST" > "HOL4Base.rich_list.BUTLAST"
+ "BUTFIRSTN_SNOC" > "HOL4Base.rich_list.BUTFIRSTN_SNOC"
+ "BUTFIRSTN_SEG" > "HOL4Base.rich_list.BUTFIRSTN_SEG"
+ "BUTFIRSTN_REVERSE" > "HOL4Base.rich_list.BUTFIRSTN_REVERSE"
+ "BUTFIRSTN_LENGTH_NIL" > "HOL4Base.rich_list.BUTFIRSTN_LENGTH_NIL"
+ "BUTFIRSTN_LENGTH_APPEND" > "HOL4Base.rich_list.BUTFIRSTN_LENGTH_APPEND"
+ "BUTFIRSTN_LASTN" > "HOL4Base.rich_list.BUTFIRSTN_LASTN"
+ "BUTFIRSTN_BUTFIRSTN" > "HOL4Base.rich_list.BUTFIRSTN_BUTFIRSTN"
+ "BUTFIRSTN_APPEND2" > "HOL4Base.rich_list.BUTFIRSTN_APPEND2"
+ "BUTFIRSTN_APPEND1" > "HOL4Base.rich_list.BUTFIRSTN_APPEND1"
+ "BUTFIRSTN" > "HOL4Base.rich_list.BUTFIRSTN"
+ "ASSOC_FOLDR_FLAT" > "HOL4Base.rich_list.ASSOC_FOLDR_FLAT"
+ "ASSOC_FOLDL_FLAT" > "HOL4Base.rich_list.ASSOC_FOLDL_FLAT"
+ "ASSOC_APPEND" > "HOL4Base.rich_list.ASSOC_APPEND"
+ "APPEND_SNOC" > "HOL4Base.rich_list.APPEND_SNOC"
+ "APPEND_NIL" > "HOL4Base.rich_list.APPEND_NIL"
+ "APPEND_LENGTH_EQ" > "HOL4Base.rich_list.APPEND_LENGTH_EQ"
+ "APPEND_FOLDR" > "HOL4Base.rich_list.APPEND_FOLDR"
+ "APPEND_FOLDL" > "HOL4Base.rich_list.APPEND_FOLDL"
+ "APPEND_FIRSTN_LASTN" > "HOL4Base.rich_list.APPEND_FIRSTN_LASTN"
+ "APPEND_FIRSTN_BUTFIRSTN" > "HOL4Base.rich_list.APPEND_FIRSTN_BUTFIRSTN"
+ "APPEND_BUTLAST_LAST" > "List.append_butlast_last_id"
+ "APPEND_BUTLASTN_LASTN" > "HOL4Base.rich_list.APPEND_BUTLASTN_LASTN"
+ "APPEND_BUTLASTN_BUTFIRSTN" > "HOL4Base.rich_list.APPEND_BUTLASTN_BUTFIRSTN"
+ "APPEND_ASSOC" > "List.append_assoc"
+ "APPEND" > "HOL4Compat.APPEND"
+ "AND_EL_def" > "HOL4Base.rich_list.AND_EL_def"
+ "AND_EL_FOLDR" > "HOL4Base.rich_list.AND_EL_FOLDR"
+ "AND_EL_FOLDL" > "HOL4Base.rich_list.AND_EL_FOLDL"
+ "AND_EL_DEF" > "HOL4Base.rich_list.AND_EL_DEF"
+ "ALL_EL_SNOC" > "HOL4Base.rich_list.ALL_EL_SNOC"
+ "ALL_EL_SEG" > "HOL4Base.rich_list.ALL_EL_SEG"
+ "ALL_EL_REVERSE" > "HOL4Base.rich_list.ALL_EL_REVERSE"
+ "ALL_EL_REPLICATE" > "HOL4Base.rich_list.ALL_EL_REPLICATE"
+ "ALL_EL_MAP" > "HOL4Base.rich_list.ALL_EL_MAP"
+ "ALL_EL_LASTN" > "HOL4Base.rich_list.ALL_EL_LASTN"
+ "ALL_EL_FOLDR_MAP" > "HOL4Base.rich_list.ALL_EL_FOLDR_MAP"
+ "ALL_EL_FOLDR" > "HOL4Base.rich_list.ALL_EL_FOLDR"
+ "ALL_EL_FOLDL_MAP" > "HOL4Base.rich_list.ALL_EL_FOLDL_MAP"
+ "ALL_EL_FOLDL" > "HOL4Base.rich_list.ALL_EL_FOLDL"
+ "ALL_EL_FIRSTN" > "HOL4Base.rich_list.ALL_EL_FIRSTN"
+ "ALL_EL_CONJ" > "HOL4Base.list.EVERY_CONJ"
+ "ALL_EL_BUTLASTN" > "HOL4Base.rich_list.ALL_EL_BUTLASTN"
+ "ALL_EL_BUTFIRSTN" > "HOL4Base.rich_list.ALL_EL_BUTFIRSTN"
+ "ALL_EL_APPEND" > "List.list_all_append"
+ "ALL_EL" > "HOL4Compat.EVERY_DEF"
+
+end