equal
deleted
inserted
replaced
512 val qalpha_bns = map #qconst qalpha_bns_info |
512 val qalpha_bns = map #qconst qalpha_bns_info |
513 |
513 |
514 (* lifting of the theorems *) |
514 (* lifting of the theorems *) |
515 val _ = warning "Lifting of Theorems" |
515 val _ = warning "Lifting of Theorems" |
516 |
516 |
517 val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps |
517 val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel_def |
518 prod.cases} |
518 prod.cases} |
519 |
519 |
520 val ((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), lthyA) = |
520 val ((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), lthyA) = |
521 if get_STEPS lthy > 26 |
521 if get_STEPS lthy > 26 |
522 then |
522 then |