537 |> lift_thms qtys [] raw_size_eqvt |
537 |> lift_thms qtys [] raw_size_eqvt |
538 ||>> lift_thms qtys [] [raw_induct_thm] |
538 ||>> lift_thms qtys [] [raw_induct_thm] |
539 ||>> lift_thms qtys [] raw_exhaust_thms |
539 ||>> lift_thms qtys [] raw_exhaust_thms |
540 else raise TEST lthyA |
540 else raise TEST lthyA |
541 |
541 |
|
542 val qinducts = Project_Rule.projections lthyA qinduct |
|
543 |
542 (* supports lemmas *) |
544 (* supports lemmas *) |
543 val qsupports_thms = |
545 val qsupports_thms = |
544 if get_STEPS lthy > 28 |
546 if get_STEPS lthy > 28 |
545 then prove_supports lthyB qperm_simps qtrms |
547 then prove_supports lthyB qperm_simps qtrms |
546 else raise TEST lthyB |
548 else raise TEST lthyB |
571 ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) |
573 ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) |
572 ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) |
574 ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) |
573 ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) |
575 ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) |
574 ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt) |
576 ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt) |
575 ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) |
577 ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) |
|
578 ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts) |
576 ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts) |
579 ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts) |
577 ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) |
580 ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) |
578 ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) |
581 ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) |
579 in |
582 in |
580 (0, lthy9') |
583 (0, lthy9') |