src/HOL/Import/HOL/list.imp

renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;

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" > "List.op 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" > "HOL4Compat.list_exists"
  "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.unzip.induct"
  "list_distinct" > "List.list.simps_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.unzip.induct"
  "list_CASES" > "HOL4Compat.list_CASES"
  "list_Axiom_old" > "HOL4Compat.list_Axiom_old"
  "list_Axiom" > "HOL4Compat.list_Axiom"
  "list_11" > "List.list.simps_3"
  "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.simps_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.simps_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" > "HOL4Base.list.EXISTS_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.simps_3"
  "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