equal
deleted
inserted
replaced
527 val qpermute_bn_thms = |
527 val qpermute_bn_thms = |
528 if get_STEPS lthy > 33 |
528 if get_STEPS lthy > 33 |
529 then prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qfv_qbn_eqvts lthyC |
529 then prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qfv_qbn_eqvts lthyC |
530 else [] |
530 else [] |
531 |
531 |
|
532 (* proving the strong exhausts and induct lemmas *) |
532 val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts bclauses qbn_finite_thms qeq_iffs' |
533 val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts bclauses qbn_finite_thms qeq_iffs' |
533 qfv_qbn_eqvts qpermute_bn_thms qperm_bn_alpha_thms |
534 qfv_qbn_eqvts qpermute_bn_thms qperm_bn_alpha_thms |
|
535 |
|
536 val qstrong_induct_thm = prove_strong_induct lthyC qinduct qexhausts bclauses |
534 |
537 |
535 |
538 |
536 (* noting the theorems *) |
539 (* noting the theorems *) |
537 |
540 |
538 (* generating the prefix for the theorem names *) |
541 (* generating the prefix for the theorem names *) |