520 ||>> Local_Theory.note ((thms_suffix "strong_exhaust", [case_names_attr]), qstrong_exhaust_thms) |
520 ||>> Local_Theory.note ((thms_suffix "strong_exhaust", [case_names_attr]), qstrong_exhaust_thms) |
521 ||>> Local_Theory.note ((thms_suffix "strong_induct", [case_names_attr]), qstrong_induct_thms) |
521 ||>> Local_Theory.note ((thms_suffix "strong_induct", [case_names_attr]), qstrong_induct_thms) |
522 ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) |
522 ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) |
523 ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) |
523 ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) |
524 ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs) |
524 ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs) |
525 ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs) |
525 ||>> Local_Theory.note ((thms_suffix "fresh", [simp_attr]), qfresh_constrs) |
526 ||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps) |
526 ||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps) |
527 ||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms) |
527 ||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms) |
528 ||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms) |
528 ||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms) |
529 ||>> Local_Theory.note ((thms_suffix "permute_bn", []), qpermute_bn_thms) |
529 ||>> Local_Theory.note ((thms_suffix "permute_bn", []), qpermute_bn_thms) |
530 ||>> Local_Theory.note ((thms_suffix "alpha_refl", []), qalpha_refl_thms) |
530 ||>> Local_Theory.note ((thms_suffix "alpha_refl", []), qalpha_refl_thms) |