(** legacy ML bindings **) val Cons_eq_appendI = thm "Cons_eq_appendI"; val Cons_in_lex = thm "Cons_in_lex"; val Nil2_notin_lex = thm "Nil2_notin_lex"; val Nil_eq_concat_conv = thm "Nil_eq_concat_conv"; val Nil_is_append_conv = thm "Nil_is_append_conv"; val Nil_is_map_conv = thm "Nil_is_map_conv"; val Nil_is_rev_conv = thm "Nil_is_rev_conv"; val Nil_notin_lex = thm "Nil_notin_lex"; val all_nth_imp_all_set = thm "all_nth_imp_all_set"; val all_set_conv_all_nth = thm "all_set_conv_all_nth"; val append1_eq_conv = thm "append1_eq_conv"; val append_Cons = thm "append_Cons"; val append_Nil = thm "append_Nil"; val append_Nil2 = thm "append_Nil2"; val append_assoc = thm "append_assoc"; val append_butlast_last_id = thm "append_butlast_last_id"; val append_eq_appendI = thm "append_eq_appendI"; val append_eq_append_conv = thm "append_eq_append_conv"; val append_eq_conv_conj = thm "append_eq_conv_conj"; val append_in_lists_conv = thm "append_in_lists_conv"; val append_is_Nil_conv = thm "append_is_Nil_conv"; val append_same_eq = thm "append_same_eq"; val append_self_conv = thm "append_self_conv"; val append_self_conv2 = thm "append_self_conv2"; val append_take_drop_id = thm "append_take_drop_id"; val butlast_append = thm "butlast_append"; val butlast_snoc = thm "butlast_snoc"; val concat_append = thm "concat_append"; val concat_eq_Nil_conv = thm "concat_eq_Nil_conv"; val distinct_append = thm "distinct_append"; val distinct_filter = thm "distinct_filter"; val distinct_remdups = thm "distinct_remdups"; val dropWhile_append1 = thm "dropWhile_append1"; val dropWhile_append2 = thm "dropWhile_append2"; val drop_0 = thm "drop_0"; val drop_Cons = thm "drop_Cons"; val drop_Cons' = thm "drop_Cons'"; val drop_Nil = thm "drop_Nil"; val drop_Suc_Cons = thm "drop_Suc_Cons"; val drop_all = thm "drop_all"; val drop_append = thm "drop_append"; val drop_drop = thm "drop_drop"; val drop_map = thm "drop_map"; val elem_le_sum = thm "elem_le_sum"; val eq_Nil_appendI = thm "eq_Nil_appendI"; val filter_False = thm "filter_False"; val filter_True = thm "filter_True"; val filter_append = thm "filter_append"; val filter_concat = thm "filter_concat"; val filter_filter = thm "filter_filter"; val filter_is_subset = thm "filter_is_subset"; val finite_set = thm "finite_set"; val foldl_Cons = thm "foldl_Cons"; val foldl_Nil = thm "foldl_Nil"; val foldl_append = thm "foldl_append"; val hd_Cons_tl = thm "hd_Cons_tl"; val hd_append = thm "hd_append"; val hd_append2 = thm "hd_append2"; val hd_replicate = thm "hd_replicate"; val in_listsD = thm "in_listsD"; val in_listsI = thm "in_listsI"; val in_lists_conv_set = thm "in_lists_conv_set"; val in_set_butlastD = thm "in_set_butlastD"; val in_set_butlast_appendI = thm "in_set_butlast_appendI"; val in_set_conv_decomp = thm "in_set_conv_decomp"; val in_set_replicateD = thm "in_set_replicateD"; val inj_map = thm "inj_map"; val inj_mapD = thm "inj_mapD"; val inj_mapI = thm "inj_mapI"; val last_replicate = thm "last_replicate"; val last_snoc = thm "last_snoc"; val length_0_conv = thm "length_0_conv"; val length_Suc_conv = thm "length_Suc_conv"; val length_append = thm "length_append"; val length_butlast = thm "length_butlast"; val length_drop = thm "length_drop"; val length_filter_le = thm "length_filter_le"; val length_greater_0_conv = thm "length_greater_0_conv"; val length_induct = thm "length_induct"; val length_list_update = thm "length_list_update"; val length_map = thm "length_map"; val length_replicate = thm "length_replicate"; val length_rev = thm "length_rev"; val length_take = thm "length_take"; val length_tl = thm "length_tl"; val length_upt = thm "length_upt"; val length_zip = thm "length_zip"; val lex_conv = thm "lex_conv"; val lex_def = thm "lex_def"; val lenlex_conv = thm "lenlex_conv"; val lenlex_def = thm "lenlex_def"; val lexn_conv = thm "lexn_conv"; val lexn_length = thm "lexn_length"; val list_all2_Cons = thm "list_all2_Cons"; val list_all2_Cons1 = thm "list_all2_Cons1"; val list_all2_Cons2 = thm "list_all2_Cons2"; val list_all2_Nil = thm "list_all2_Nil"; val list_all2_Nil2 = thm "list_all2_Nil2"; val list_all2_append1 = thm "list_all2_append1"; val list_all2_append2 = thm "list_all2_append2"; val list_all2_conv_all_nth = thm "list_all2_conv_all_nth"; val list_all2_def = thm "list_all2_def"; val list_all2_lengthD = thm "list_all2_lengthD"; val list_all2_rev = thm "list_all2_rev"; val list_all2_trans = thm "list_all2_trans"; val list_all_append = thm "list_all_append"; val list_all_iff = thm "list_all_iff"; val list_ball_nth = thm "list_ball_nth"; val list_update_overwrite = thm "list_update_overwrite"; val list_update_same_conv = thm "list_update_same_conv"; val listsE = thm "listsE"; val lists_IntI = thm "lists_IntI"; val lists_Int_eq = thm "lists_Int_eq"; val lists_mono = thm "lists_mono"; val map_Suc_upt = thm "map_Suc_upt"; val map_append = thm "map_append"; val map_compose = thm "map_compose"; val map_concat = thm "map_concat"; val map_cong = thm "map_cong"; val map_eq_Cons_conv = thm "map_eq_Cons_conv"; val map_ext = thm "map_ext"; val map_ident = thm "map_ident"; val map_injective = thm "map_injective"; val map_is_Nil_conv = thm "map_is_Nil_conv"; val map_replicate = thm "map_replicate"; val neq_Nil_conv = thm "neq_Nil_conv"; val not_Cons_self = thm "not_Cons_self"; val not_Cons_self2 = thm "not_Cons_self2"; val nth_Cons = thm "nth_Cons"; val nth_Cons' = thm "nth_Cons'"; val nth_Cons_0 = thm "nth_Cons_0"; val nth_Cons_Suc = thm "nth_Cons_Suc"; val nth_append = thm "nth_append"; val nth_drop = thm "nth_drop"; val nth_equalityI = thm "nth_equalityI"; val nth_list_update = thm "nth_list_update"; val nth_list_update_eq = thm "nth_list_update_eq"; val nth_list_update_neq = thm "nth_list_update_neq"; val nth_map = thm "nth_map"; val nth_map_upt = thm "nth_map_upt"; val nth_mem = thm "nth_mem"; val nth_replicate = thm "nth_replicate"; val nth_take = thm "nth_take"; val nth_take_lemma = thm "nth_take_lemma"; val nth_upt = thm "nth_upt"; val nth_zip = thm "nth_zip"; val replicate_0 = thm "replicate_0"; val replicate_Suc = thm "replicate_Suc"; val replicate_add = thm "replicate_add"; val replicate_app_Cons_same = thm "replicate_app_Cons_same"; val rev_append = thm "rev_append"; val rev_concat = thm "rev_concat"; val rev_drop = thm "rev_drop"; val rev_exhaust = thm "rev_exhaust"; val rev_induct = thm "rev_induct"; val rev_is_Nil_conv = thm "rev_is_Nil_conv"; val rev_is_rev_conv = thm "rev_is_rev_conv"; val rev_map = thm "rev_map"; val rev_replicate = thm "rev_replicate"; val rev_rev_ident = thm "rev_rev_ident"; val rev_take = thm "rev_take"; val same_append_eq = thm "same_append_eq"; val self_append_conv = thm "self_append_conv"; val self_append_conv2 = thm "self_append_conv2"; val set_append = thm "set_append"; val set_concat = thm "set_concat"; val set_conv_nth = thm "set_conv_nth"; val set_empty = thm "set_empty"; val set_filter = thm "set_filter"; val set_map = thm "set_map"; val mem_ii = thm "mem_iff"; val set_remdups = thm "set_remdups"; val set_replicate = thm "set_replicate"; val set_replicate_conv_if = thm "set_replicate_conv_if"; val set_rev = thm "set_rev"; val set_subset_Cons = thm "set_subset_Cons"; val set_take_whileD = thm "set_take_whileD"; val set_update_subsetI = thm "set_update_subsetI"; val set_update_subset_insert = thm "set_update_subset_insert"; val set_upt = thm "set_upt"; val set_zip = thm "set_zip"; val start_le_sum = thm "start_le_sum"; val sublist_Cons = thm "sublist_Cons"; val sublist_append = thm "sublist_append"; val sublist_def = thm "sublist_def"; val sublist_empty = thm "sublist_empty"; val sublist_nil = thm "sublist_nil"; val sublist_shift_lemma = thm "sublist_shift_lemma"; val sublist_singleton = thm "sublist_singleton"; val sublist_upt_eq_take = thm "sublist_upt_eq_take"; val sum_eq_0_conv = thm "sum_eq_0_conv"; val takeWhile_append1 = thm "takeWhile_append1"; val takeWhile_append2 = thm "takeWhile_append2"; val takeWhile_dropWhile_id = thm "takeWhile_dropWhile_id"; val takeWhile_tail = thm "takeWhile_tail"; val take_0 = thm "take_0"; val take_Cons = thm "take_Cons"; val take_Cons' = thm "take_Cons'"; val take_Nil = thm "take_Nil"; val take_Suc_Cons = thm "take_Suc_Cons"; val take_all = thm "take_all"; val take_append = thm "take_append"; val take_drop = thm "take_drop"; val take_equalityI = thm "take_equalityI"; val take_map = thm "take_map"; val take_take = thm "take_take"; val take_upt = thm "take_upt"; val tl_append = thm "tl_append"; val tl_append2 = thm "tl_append2"; val tl_replicate = thm "tl_replicate"; val update_zip = thm "update_zip"; val upt_0 = thm "upt_0"; val upt_Suc = thm "upt_Suc"; val upt_Suc_append = thm "upt_Suc_append"; val upt_add_eq_append = thm "upt_add_eq_append"; val upt_conv_Cons = thm "upt_conv_Cons"; val upt_conv_Nil = thm "upt_conv_Nil"; val upt_rec = thm "upt_rec"; val wf_lex = thm "wf_lex"; val wf_lenlex = thm "wf_lenlex"; val wf_lexn = thm "wf_lexn"; val zip_Cons_Cons = thm "zip_Cons_Cons"; val zip_Nil = thm "zip_Nil"; val zip_append = thm "zip_append"; val zip_append1 = thm "zip_append1"; val zip_append2 = thm "zip_append2"; val zip_replicate = thm "zip_replicate"; val zip_rev = thm "zip_rev"; val zip_update = thm "zip_update";