equal
deleted
inserted
replaced
610 ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts) |
610 ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts) |
611 ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) |
611 ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) |
612 ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) |
612 ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) |
613 ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs) |
613 ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs) |
614 ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs) |
614 ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs) |
|
615 ||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros) |
615 in |
616 in |
616 (0, lthy9') |
617 (0, lthy9') |
617 end handle TEST ctxt => (0, ctxt) |
618 end handle TEST ctxt => (0, ctxt) |
618 *} |
619 *} |
619 |
620 |