src/HOL/List.ML

 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_Cons = thm "list_all_Cons";
-val list_all_Nil = thm "list_all_Nil";
 val list_all_append = thm "list_all_append";
-val list_all_conv = thm "list_all_conv";
+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 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 set_mem_eq = thm "set_mem_eq";
+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";