src/HOL/Import/HOL4/Generated/list.imp

merged;

import

import_segment "hol4"

def_maps
  "EL" > "EL_def"

type_maps
  "list" > "List.list"

const_maps
  "list_size" > "Compatibility.list_size"
  "list_case" > "List.list.list_case"
  "ZIP" > "Compatibility.ZIP"
  "UNZIP" > "Compatibility.unzip"
  "TL" > "List.tl"
  "SUM" > "Compatibility.sum"
  "REVERSE" > "List.rev"
  "REPLICATE" > "List.replicate"
  "NULL" > "List.null"
  "NIL" > "List.list.Nil"
  "MEM" > "Compatibility.list_mem"
  "MAP2" > "Compatibility.map2"
  "MAP" > "List.map"
  "LENGTH" > "Nat.size_class.size"
  "LAST" > "List.last"
  "HD" > "List.hd"
  "FRONT" > "List.butlast"
  "FOLDR" > "Compatibility.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" > "Compatibility.list_size_def'"
  "list_size_cong" > "HOL4Base.list.list_size_cong"
  "list_nchotomy" > "Compatibility.list_CASES"
  "list_induction" > "Compatibility.list_INDUCT"
  "list_distinct" > "List.list.distinct_1"
  "list_case_def" > "Compatibility.list_case_def"
  "list_case_cong" > "Compatibility.list_case_cong"
  "list_case_compute" > "HOL4Base.list.list_case_compute"
  "list_INDUCT" > "Compatibility.list_INDUCT"
  "list_CASES" > "Compatibility.list_CASES"
  "list_Axiom_old" > "Compatibility.list_Axiom_old"
  "list_Axiom" > "Compatibility.list_Axiom"
  "list_11" > "List.list.inject"
  "ZIP_UNZIP" > "HOL4Base.list.ZIP_UNZIP"
  "ZIP_MAP" > "HOL4Base.list.ZIP_MAP"
  "ZIP" > "Compatibility.ZIP"
  "WF_LIST_PRED" > "HOL4Base.list.WF_LIST_PRED"
  "UNZIP_ZIP" > "HOL4Base.list.UNZIP_ZIP"
  "UNZIP" > "Compatibility.UNZIP"
  "TL" > "List.tl.simps_2"
  "SUM" > "Compatibility.SUM"
  "REVERSE_REVERSE" > "List.rev_rev_ident"
  "REVERSE_DEF" > "Compatibility.REVERSE"
  "REVERSE_APPEND" > "List.rev_append"
  "NULL_DEF" > "Compatibility.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" > "Compatibility.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" > "Compatibility.MAP2"
  "MAP" > "Compatibility.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" > "Compatibility.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" > "Compatibility.FOLDR"
  "FOLDL_CONG" > "HOL4Base.list.FOLDL_CONG"
  "FOLDL" > "Compatibility.FOLDL"
  "FLAT" > "Compatibility.FLAT"
  "FILTER" > "Compatibility.FILTER"
  "EXISTS_MEM" > "HOL4Base.list.EXISTS_MEM"
  "EXISTS_DEF" > "Compatibility.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" > "Compatibility.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" > "Compatibility.APPEND"

ignore_thms
  "list_repfns"
  "list_TY_DEF"
  "list1_def"
  "list0_def"
  "NIL"
  "CONS_def"

end