equal
deleted
inserted
replaced
432 then map mk_alpha_permute_rsp alpha_eqvt |
432 then map mk_alpha_permute_rsp alpha_eqvt |
433 else raise TEST lthy6 |
433 else raise TEST lthy6 |
434 |
434 |
435 val alpha_bn_rsp = |
435 val alpha_bn_rsp = |
436 if get_STEPS lthy > 20 |
436 if get_STEPS lthy > 20 |
437 then raw_alpha_bn_rsp alpha_bn_equivp_thms alpha_bn_imp_thms |
437 then raw_alpha_bn_rsp alpha_bn_trms alpha_bn_equivp_thms alpha_bn_imp_thms |
438 else raise TEST lthy6 |
438 else raise TEST lthy6 |
439 |
439 |
440 (* noting the quot_respects lemmas *) |
440 (* noting the quot_respects lemmas *) |
441 val (_, lthy6a) = |
441 val (_, lthy6a) = |
442 if get_STEPS lthy > 21 |
442 if get_STEPS lthy > 21 |