397 val qfv_bns = map #qconst qfv_bns_info |
397 val qfv_bns = map #qconst qfv_bns_info |
398 val qalpha_bns = map #qconst qalpha_bns_info |
398 val qalpha_bns = map #qconst qalpha_bns_info |
399 val qperm_bns = map #qconst qperm_bns_info |
399 val qperm_bns = map #qconst qperm_bns_info |
400 |
400 |
401 val _ = trace_msg (K "Lifting of theorems...") |
401 val _ = trace_msg (K "Lifting of theorems...") |
402 val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel_def |
402 val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def rel_prod_def |
403 prod.cases} |
403 prod.case} |
404 |
404 |
405 val ([ qdistincts, qeq_iffs, qfv_defs, qbn_defs, qperm_simps, qfv_qbn_eqvts, |
405 val ([ qdistincts, qeq_iffs, qfv_defs, qbn_defs, qperm_simps, qfv_qbn_eqvts, |
406 qbn_inducts, qsize_eqvt, [qinduct], qexhausts, qsize_simps, qperm_bn_simps, |
406 qbn_inducts, qsize_eqvt, [qinduct], qexhausts, qsize_simps, qperm_bn_simps, |
407 qalpha_refl_thms, qalpha_sym_thms, qalpha_trans_thms ], lthyB) = |
407 qalpha_refl_thms, qalpha_sym_thms, qalpha_trans_thms ], lthyB) = |
408 lthy9a |
408 lthy9a |