equal
deleted
inserted
replaced
545 val qsupports_thms = |
545 val qsupports_thms = |
546 if get_STEPS lthy > 28 |
546 if get_STEPS lthy > 28 |
547 then prove_supports lthyB qperm_simps qtrms |
547 then prove_supports lthyB qperm_simps qtrms |
548 else raise TEST lthyB |
548 else raise TEST lthyB |
549 |
549 |
|
550 val qfsupp_thms = |
|
551 if get_STEPS lthy > 29 |
|
552 then prove_fsupp lthyB qtys qinduct qsupports_thms |
|
553 else raise TEST lthyB |
|
554 |
550 |
555 |
551 (* noting the theorems *) |
556 (* noting the theorems *) |
552 |
557 |
553 (* generating the prefix for the theorem names *) |
558 (* generating the prefix for the theorem names *) |
554 val thms_name = |
559 val thms_name = |
564 ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) |
569 ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) |
565 ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt) |
570 ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt) |
566 ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) |
571 ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) |
567 ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts) |
572 ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts) |
568 ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) |
573 ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) |
569 |
574 ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) |
570 in |
575 in |
571 (0, lthy9') |
576 (0, lthy9') |
572 end handle TEST ctxt => (0, ctxt) |
577 end handle TEST ctxt => (0, ctxt) |
573 *} |
578 *} |
574 |
579 |