HOL/Import: Update HOL4 generated files to current Isabelle.
import
import_segment "hol4"
def_maps
"EL" > "EL_def"
type_maps
"list" > "List.list"
const_maps
"list_size" > "HOL4Compat.list_size"
"list_case" > "List.list.list_case"
"ZIP" > "HOL4Compat.ZIP"
"UNZIP" > "HOL4Compat.unzip"
"TL" > "List.tl"
"SUM" > "HOL4Compat.sum"
"REVERSE" > "List.rev"
"REPLICATE" > "List.replicate"
"NULL" > "List.null"
"NIL" > "List.list.Nil"
"MEM" > "HOL4Compat.list_mem"
"MAP2" > "HOL4Compat.map2"
"MAP" > "List.map"
"LENGTH" > "Nat.size_class.size"
"LAST" > "List.last"
"HD" > "List.hd"
"FRONT" > "List.butlast"
"FOLDR" > "HOL4Compat.FOLDR"
"FOLDL" > "List.foldl"
"FLAT" > "List.concat"
"FILTER" > "List.filter"
"EXISTS" > "List.list_ex"
"EVERY" > "List.list_all"
"CONS" > "List.list.Cons"
"APPEND" > "List.append"
thm_maps
"list_size_def" > "HOL4Compat.list_size_def'"
"list_size_cong" > "HOL4Base.list.list_size_cong"
"list_nchotomy" > "HOL4Compat.list_CASES"
"list_induction" > "HOL4Compat.list_INDUCT"
"list_distinct" > "List.list.distinct_1"
"list_case_def" > "HOL4Compat.list_case_def"
"list_case_cong" > "HOL4Compat.list_case_cong"
"list_case_compute" > "HOL4Base.list.list_case_compute"
"list_INDUCT" > "HOL4Compat.list_INDUCT"
"list_CASES" > "HOL4Compat.list_CASES"
"list_Axiom_old" > "HOL4Compat.list_Axiom_old"
"list_Axiom" > "HOL4Compat.list_Axiom"
"list_11" > "List.list.inject"
"ZIP_UNZIP" > "HOL4Base.list.ZIP_UNZIP"
"ZIP_MAP" > "HOL4Base.list.ZIP_MAP"
"ZIP" > "HOL4Compat.ZIP"
"WF_LIST_PRED" > "HOL4Base.list.WF_LIST_PRED"
"UNZIP_ZIP" > "HOL4Base.list.UNZIP_ZIP"
"UNZIP" > "HOL4Compat.UNZIP"
"TL" > "List.tl.simps_2"
"SUM" > "HOL4Compat.SUM"
"REVERSE_REVERSE" > "List.rev_rev_ident"
"REVERSE_DEF" > "HOL4Compat.REVERSE"
"REVERSE_APPEND" > "List.rev_append"
"NULL_DEF" > "HOL4Compat.NULL_DEF"
"NULL" > "HOL4Base.list.NULL"
"NOT_NIL_CONS" > "List.list.distinct_1"
"NOT_EXISTS" > "HOL4Base.list.NOT_EXISTS"
"NOT_EVERY" > "HOL4Base.list.NOT_EVERY"
"NOT_EQ_LIST" > "HOL4Base.list.NOT_EQ_LIST"
"NOT_CONS_NIL" > "List.list.distinct_2"
"MEM_ZIP" > "HOL4Base.list.MEM_ZIP"
"MEM_MAP" > "HOL4Base.list.MEM_MAP"
"MEM_EL" > "HOL4Base.list.MEM_EL"
"MEM_APPEND" > "HOL4Base.list.MEM_APPEND"
"MEM" > "HOL4Compat.MEM"
"MAP_EQ_NIL" > "HOL4Base.list.MAP_EQ_NIL"
"MAP_CONG" > "HOL4Base.list.MAP_CONG"
"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" > "HOL4Base.list.LENGTH_UNZIP"
"LENGTH_NIL" > "List.length_0_conv"
"LENGTH_MAP" > "List.length_map"
"LENGTH_EQ_NIL" > "HOL4Base.list.LENGTH_EQ_NIL"
"LENGTH_EQ_CONS" > "HOL4Base.list.LENGTH_EQ_CONS"
"LENGTH_CONS" > "HOL4Base.list.LENGTH_CONS"
"LENGTH_APPEND" > "List.length_append"
"LENGTH" > "HOL4Compat.LENGTH"
"LAST_DEF" > "List.last.simps"
"LAST_CONS" > "HOL4Base.list.LAST_CONS"
"HD" > "List.hd.simps"
"FRONT_DEF" > "List.butlast.simps_2"
"FRONT_CONS" > "HOL4Base.list.FRONT_CONS"
"FOLDR_CONG" > "HOL4Base.list.FOLDR_CONG"
"FOLDR" > "HOL4Compat.FOLDR"
"FOLDL_CONG" > "HOL4Base.list.FOLDL_CONG"
"FOLDL" > "HOL4Compat.FOLDL"
"FLAT" > "HOL4Compat.FLAT"
"FILTER" > "HOL4Compat.FILTER"
"EXISTS_MEM" > "HOL4Base.list.EXISTS_MEM"
"EXISTS_DEF" > "HOL4Compat.list_exists_DEF"
"EXISTS_CONG" > "HOL4Base.list.EXISTS_CONG"
"EXISTS_APPEND" > "List.list_ex_append"
"EVERY_MONOTONIC" > "HOL4Base.list.EVERY_MONOTONIC"
"EVERY_MEM" > "HOL4Base.list.EVERY_MEM"
"EVERY_EL" > "HOL4Base.list.EVERY_EL"
"EVERY_DEF" > "HOL4Compat.EVERY_DEF"
"EVERY_CONJ" > "HOL4Base.list.EVERY_CONJ"
"EVERY_CONG" > "HOL4Base.list.EVERY_CONG"
"EVERY_APPEND" > "List.list_all_append"
"EQ_LIST" > "HOL4Base.list.EQ_LIST"
"EL_compute" > "HOL4Base.list.EL_compute"
"EL_ZIP" > "HOL4Base.list.EL_ZIP"
"EL" > "HOL4Base.list.EL"
"CONS_ACYCLIC" > "HOL4Base.list.CONS_ACYCLIC"
"CONS_11" > "List.list.inject"
"CONS" > "HOL4Base.list.CONS"
"APPEND_eq_NIL" > "HOL4Base.list.APPEND_eq_NIL"
"APPEND_NIL" > "List.append_Nil2"
"APPEND_FRONT_LAST" > "List.append_butlast_last_id"
"APPEND_ASSOC" > "List.append_assoc"
"APPEND_11" > "HOL4Base.list.APPEND_11"
"APPEND" > "HOL4Compat.APPEND"
ignore_thms
"list_repfns"
"list_TY_DEF"
"list1_def"
"list0_def"
"NIL"
"CONS_def"
end