renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
import
import_segment "hol4"
def_maps
"algebra_canon" > "algebra_canon_primdef"
"alg_twinfree" > "alg_twinfree_primdef"
"alg_twin" > "alg_twin_primdef"
"alg_sorted" > "alg_sorted_primdef"
"alg_prefixfree" > "alg_prefixfree_primdef"
"alg_order_tupled" > "alg_order_tupled_def"
"alg_order" > "alg_order_primdef"
"alg_longest" > "alg_longest_primdef"
"alg_canon_prefs" > "alg_canon_prefs_primdef"
"alg_canon_merge" > "alg_canon_merge_primdef"
"alg_canon_find" > "alg_canon_find_primdef"
"alg_canon2" > "alg_canon2_primdef"
"alg_canon1" > "alg_canon1_primdef"
"alg_canon" > "alg_canon_primdef"
const_maps
"algebra_canon" > "HOL4Prob.prob_canon.algebra_canon"
"alg_twinfree" > "HOL4Prob.prob_canon.alg_twinfree"
"alg_twin" > "HOL4Prob.prob_canon.alg_twin"
"alg_sorted" > "HOL4Prob.prob_canon.alg_sorted"
"alg_prefixfree" > "HOL4Prob.prob_canon.alg_prefixfree"
"alg_order_tupled" > "HOL4Prob.prob_canon.alg_order_tupled"
"alg_order" > "HOL4Prob.prob_canon.alg_order"
"alg_longest" > "HOL4Prob.prob_canon.alg_longest"
"alg_canon2" > "HOL4Prob.prob_canon.alg_canon2"
"alg_canon1" > "HOL4Prob.prob_canon.alg_canon1"
"alg_canon" > "HOL4Prob.prob_canon.alg_canon"
thm_maps
"algebra_canon_primdef" > "HOL4Prob.prob_canon.algebra_canon_primdef"
"algebra_canon_def" > "HOL4Prob.prob_canon.algebra_canon_def"
"alg_twinfree_primitive_def" > "HOL4Prob.prob_canon.alg_twinfree_primitive_def"
"alg_twinfree_primdef" > "HOL4Prob.prob_canon.alg_twinfree_primdef"
"alg_twinfree_ind" > "HOL4Prob.prob_canon.alg_twinfree_ind"
"alg_twinfree_def" > "HOL4Prob.prob_canon.alg_twinfree_def"
"alg_twin_primdef" > "HOL4Prob.prob_canon.alg_twin_primdef"
"alg_twin_def" > "HOL4Prob.prob_canon.alg_twin_def"
"alg_sorted_primitive_def" > "HOL4Prob.prob_canon.alg_sorted_primitive_def"
"alg_sorted_primdef" > "HOL4Prob.prob_canon.alg_sorted_primdef"
"alg_sorted_ind" > "HOL4Prob.prob_canon.alg_sorted_ind"
"alg_sorted_def" > "HOL4Prob.prob_canon.alg_sorted_def"
"alg_prefixfree_primitive_def" > "HOL4Prob.prob_canon.alg_prefixfree_primitive_def"
"alg_prefixfree_primdef" > "HOL4Prob.prob_canon.alg_prefixfree_primdef"
"alg_prefixfree_ind" > "HOL4Prob.prob_canon.alg_prefixfree_ind"
"alg_prefixfree_def" > "HOL4Prob.prob_canon.alg_prefixfree_def"
"alg_order_tupled_primitive_def" > "HOL4Prob.prob_canon.alg_order_tupled_primitive_def"
"alg_order_tupled_def" > "HOL4Prob.prob_canon.alg_order_tupled_def"
"alg_order_primdef" > "HOL4Prob.prob_canon.alg_order_primdef"
"alg_order_ind" > "HOL4Prob.prob_canon.alg_order_ind"
"alg_order_def" > "HOL4Prob.prob_canon.alg_order_def"
"alg_order_curried_def" > "HOL4Prob.prob_canon.alg_order_curried_def"
"alg_longest_primdef" > "HOL4Prob.prob_canon.alg_longest_primdef"
"alg_longest_def" > "HOL4Prob.prob_canon.alg_longest_def"
"alg_canon_primdef" > "HOL4Prob.prob_canon.alg_canon_primdef"
"alg_canon_prefs_def" > "HOL4Prob.prob_canon.alg_canon_prefs_def"
"alg_canon_merge_def" > "HOL4Prob.prob_canon.alg_canon_merge_def"
"alg_canon_find_def" > "HOL4Prob.prob_canon.alg_canon_find_def"
"alg_canon_def" > "HOL4Prob.prob_canon.alg_canon_def"
"alg_canon2_primdef" > "HOL4Prob.prob_canon.alg_canon2_primdef"
"alg_canon2_def" > "HOL4Prob.prob_canon.alg_canon2_def"
"alg_canon1_primdef" > "HOL4Prob.prob_canon.alg_canon1_primdef"
"alg_canon1_def" > "HOL4Prob.prob_canon.alg_canon1_def"
"MEM_NIL_STEP" > "HOL4Prob.prob_canon.MEM_NIL_STEP"
"ALG_TWIN_SING" > "HOL4Prob.prob_canon.ALG_TWIN_SING"
"ALG_TWIN_REDUCE" > "HOL4Prob.prob_canon.ALG_TWIN_REDUCE"
"ALG_TWIN_NIL" > "HOL4Prob.prob_canon.ALG_TWIN_NIL"
"ALG_TWIN_CONS" > "HOL4Prob.prob_canon.ALG_TWIN_CONS"
"ALG_TWINS_PREFIX" > "HOL4Prob.prob_canon.ALG_TWINS_PREFIX"
"ALG_TWINFREE_TLS" > "HOL4Prob.prob_canon.ALG_TWINFREE_TLS"
"ALG_TWINFREE_TL" > "HOL4Prob.prob_canon.ALG_TWINFREE_TL"
"ALG_TWINFREE_STEP2" > "HOL4Prob.prob_canon.ALG_TWINFREE_STEP2"
"ALG_TWINFREE_STEP1" > "HOL4Prob.prob_canon.ALG_TWINFREE_STEP1"
"ALG_TWINFREE_STEP" > "HOL4Prob.prob_canon.ALG_TWINFREE_STEP"
"ALG_SORTED_TLS" > "HOL4Prob.prob_canon.ALG_SORTED_TLS"
"ALG_SORTED_TL" > "HOL4Prob.prob_canon.ALG_SORTED_TL"
"ALG_SORTED_STEP" > "HOL4Prob.prob_canon.ALG_SORTED_STEP"
"ALG_SORTED_PREFIXFREE_MEM_NIL" > "HOL4Prob.prob_canon.ALG_SORTED_PREFIXFREE_MEM_NIL"
"ALG_SORTED_PREFIXFREE_EQUALITY" > "HOL4Prob.prob_canon.ALG_SORTED_PREFIXFREE_EQUALITY"
"ALG_SORTED_MONO" > "HOL4Prob.prob_canon.ALG_SORTED_MONO"
"ALG_SORTED_MIN" > "HOL4Prob.prob_canon.ALG_SORTED_MIN"
"ALG_SORTED_FILTER" > "HOL4Prob.prob_canon.ALG_SORTED_FILTER"
"ALG_SORTED_DEF_ALT" > "HOL4Prob.prob_canon.ALG_SORTED_DEF_ALT"
"ALG_SORTED_APPEND" > "HOL4Prob.prob_canon.ALG_SORTED_APPEND"
"ALG_PREFIXFREE_TLS" > "HOL4Prob.prob_canon.ALG_PREFIXFREE_TLS"
"ALG_PREFIXFREE_TL" > "HOL4Prob.prob_canon.ALG_PREFIXFREE_TL"
"ALG_PREFIXFREE_STEP" > "HOL4Prob.prob_canon.ALG_PREFIXFREE_STEP"
"ALG_PREFIXFREE_MONO" > "HOL4Prob.prob_canon.ALG_PREFIXFREE_MONO"
"ALG_PREFIXFREE_FILTER" > "HOL4Prob.prob_canon.ALG_PREFIXFREE_FILTER"
"ALG_PREFIXFREE_ELT" > "HOL4Prob.prob_canon.ALG_PREFIXFREE_ELT"
"ALG_PREFIXFREE_APPEND" > "HOL4Prob.prob_canon.ALG_PREFIXFREE_APPEND"
"ALG_ORDER_TRANS" > "HOL4Prob.prob_canon.ALG_ORDER_TRANS"
"ALG_ORDER_TOTAL" > "HOL4Prob.prob_canon.ALG_ORDER_TOTAL"
"ALG_ORDER_SNOC" > "HOL4Prob.prob_canon.ALG_ORDER_SNOC"
"ALG_ORDER_REFL" > "HOL4Prob.prob_canon.ALG_ORDER_REFL"
"ALG_ORDER_PREFIX_TRANS" > "HOL4Prob.prob_canon.ALG_ORDER_PREFIX_TRANS"
"ALG_ORDER_PREFIX_MONO" > "HOL4Prob.prob_canon.ALG_ORDER_PREFIX_MONO"
"ALG_ORDER_PREFIX_ANTI" > "HOL4Prob.prob_canon.ALG_ORDER_PREFIX_ANTI"
"ALG_ORDER_PREFIX" > "HOL4Prob.prob_canon.ALG_ORDER_PREFIX"
"ALG_ORDER_NIL" > "HOL4Prob.prob_canon.ALG_ORDER_NIL"
"ALG_ORDER_ANTISYM" > "HOL4Prob.prob_canon.ALG_ORDER_ANTISYM"
"ALG_LONGEST_TLS" > "HOL4Prob.prob_canon.ALG_LONGEST_TLS"
"ALG_LONGEST_TL" > "HOL4Prob.prob_canon.ALG_LONGEST_TL"
"ALG_LONGEST_HD" > "HOL4Prob.prob_canon.ALG_LONGEST_HD"
"ALG_LONGEST_APPEND" > "HOL4Prob.prob_canon.ALG_LONGEST_APPEND"
"ALG_CANON_SORTED_PREFIXFREE_TWINFREE" > "HOL4Prob.prob_canon.ALG_CANON_SORTED_PREFIXFREE_TWINFREE"
"ALG_CANON_PREFS_SORTED" > "HOL4Prob.prob_canon.ALG_CANON_PREFS_SORTED"
"ALG_CANON_PREFS_PREFIXFREE" > "HOL4Prob.prob_canon.ALG_CANON_PREFS_PREFIXFREE"
"ALG_CANON_PREFS_HD" > "HOL4Prob.prob_canon.ALG_CANON_PREFS_HD"
"ALG_CANON_PREFS_DELETES" > "HOL4Prob.prob_canon.ALG_CANON_PREFS_DELETES"
"ALG_CANON_PREFS_CONSTANT" > "HOL4Prob.prob_canon.ALG_CANON_PREFS_CONSTANT"
"ALG_CANON_MERGE_SORTED_PREFIXFREE_TWINFREE" > "HOL4Prob.prob_canon.ALG_CANON_MERGE_SORTED_PREFIXFREE_TWINFREE"
"ALG_CANON_MERGE_SHORTENS" > "HOL4Prob.prob_canon.ALG_CANON_MERGE_SHORTENS"
"ALG_CANON_MERGE_PREFIXFREE_PRESERVE" > "HOL4Prob.prob_canon.ALG_CANON_MERGE_PREFIXFREE_PRESERVE"
"ALG_CANON_MERGE_CONSTANT" > "HOL4Prob.prob_canon.ALG_CANON_MERGE_CONSTANT"
"ALG_CANON_IDEMPOT" > "HOL4Prob.prob_canon.ALG_CANON_IDEMPOT"
"ALG_CANON_FIND_SORTED" > "HOL4Prob.prob_canon.ALG_CANON_FIND_SORTED"
"ALG_CANON_FIND_PREFIXFREE" > "HOL4Prob.prob_canon.ALG_CANON_FIND_PREFIXFREE"
"ALG_CANON_FIND_HD" > "HOL4Prob.prob_canon.ALG_CANON_FIND_HD"
"ALG_CANON_FIND_DELETES" > "HOL4Prob.prob_canon.ALG_CANON_FIND_DELETES"
"ALG_CANON_FIND_CONSTANT" > "HOL4Prob.prob_canon.ALG_CANON_FIND_CONSTANT"
"ALG_CANON_CONSTANT" > "HOL4Prob.prob_canon.ALG_CANON_CONSTANT"
"ALG_CANON_BASIC" > "HOL4Prob.prob_canon.ALG_CANON_BASIC"
"ALG_CANON2_SORTED_PREFIXFREE_TWINFREE" > "HOL4Prob.prob_canon.ALG_CANON2_SORTED_PREFIXFREE_TWINFREE"
"ALG_CANON2_SHORTENS" > "HOL4Prob.prob_canon.ALG_CANON2_SHORTENS"
"ALG_CANON2_PREFIXFREE_PRESERVE" > "HOL4Prob.prob_canon.ALG_CANON2_PREFIXFREE_PRESERVE"
"ALG_CANON2_CONSTANT" > "HOL4Prob.prob_canon.ALG_CANON2_CONSTANT"
"ALG_CANON1_SORTED" > "HOL4Prob.prob_canon.ALG_CANON1_SORTED"
"ALG_CANON1_PREFIXFREE" > "HOL4Prob.prob_canon.ALG_CANON1_PREFIXFREE"
"ALG_CANON1_CONSTANT" > "HOL4Prob.prob_canon.ALG_CANON1_CONSTANT"
"ALGEBRA_CANON_TLS" > "HOL4Prob.prob_canon.ALGEBRA_CANON_TLS"
"ALGEBRA_CANON_TL" > "HOL4Prob.prob_canon.ALGEBRA_CANON_TL"
"ALGEBRA_CANON_STEP2" > "HOL4Prob.prob_canon.ALGEBRA_CANON_STEP2"
"ALGEBRA_CANON_STEP1" > "HOL4Prob.prob_canon.ALGEBRA_CANON_STEP1"
"ALGEBRA_CANON_STEP" > "HOL4Prob.prob_canon.ALGEBRA_CANON_STEP"
"ALGEBRA_CANON_NIL_MEM" > "HOL4Prob.prob_canon.ALGEBRA_CANON_NIL_MEM"
"ALGEBRA_CANON_INDUCTION" > "HOL4Prob.prob_canon.ALGEBRA_CANON_INDUCTION"
"ALGEBRA_CANON_DEF_ALT" > "HOL4Prob.prob_canon.ALGEBRA_CANON_DEF_ALT"
"ALGEBRA_CANON_CASES_THM" > "HOL4Prob.prob_canon.ALGEBRA_CANON_CASES_THM"
"ALGEBRA_CANON_CASES" > "HOL4Prob.prob_canon.ALGEBRA_CANON_CASES"
"ALGEBRA_CANON_BASIC" > "HOL4Prob.prob_canon.ALGEBRA_CANON_BASIC"
end