982 (exhaust_selN, exhaust_sel_thms, [exhaust_case_names_attr]), |
982 (exhaust_selN, exhaust_sel_thms, [exhaust_case_names_attr]), |
983 (expandN, expand_thms, []), |
983 (expandN, expand_thms, []), |
984 (injectN, inject_thms, iff_attrs @ inductsimp_attrs), |
984 (injectN, inject_thms, iff_attrs @ inductsimp_attrs), |
985 (nchotomyN, [nchotomy_thm], []), |
985 (nchotomyN, [nchotomy_thm], []), |
986 (selN, all_sel_thms, code_nitpicksimp_simp_attrs), |
986 (selN, all_sel_thms, code_nitpicksimp_simp_attrs), |
|
987 (splitN, [split_thm], []), |
|
988 (split_asmN, [split_asm_thm], []), |
987 (split_selN, split_sel_thms, []), |
989 (split_selN, split_sel_thms, []), |
988 (split_sel_asmN, split_sel_asm_thms, []), |
990 (split_sel_asmN, split_sel_asm_thms, []), |
989 (splitN, [split_thm], []), |
991 (split_selsN, split_sel_thms @ split_sel_asm_thms, []), |
990 (split_asmN, [split_asm_thm], []), |
992 (splitsN, [split_thm, split_asm_thm], [])] |
991 (splitsN, [split_thm, split_asm_thm], []), |
|
992 (split_selsN, split_sel_thms @ split_sel_asm_thms, [])] |
|
993 |> filter_out (null o #2) |
993 |> filter_out (null o #2) |
994 |> map (fn (thmN, thms, attrs) => |
994 |> map (fn (thmN, thms, attrs) => |
995 ((qualify true (Binding.name thmN), attrs), [(thms, [])])); |
995 ((qualify true (Binding.name thmN), attrs), [(thms, [])])); |
996 |
996 |
997 val (noted, lthy') = |
997 val (noted, lthy') = |