equal
deleted
inserted
replaced
561 |
561 |
562 (* fv - supp equality *) |
562 (* fv - supp equality *) |
563 val _ = warning "Proving Equality between fv and supp" |
563 val _ = warning "Proving Equality between fv and supp" |
564 val qfv_supp_thms = |
564 val qfv_supp_thms = |
565 if get_STEPS lthy > 31 |
565 if get_STEPS lthy > 31 |
566 then prove_fv_supp qtys qtrms qfvs qfv_bns qalpha_bns qbn_defs qfv_defs qeq_iffs |
566 then prove_fv_supp qtys qtrms qfvs qfv_bns qalpha_bns qfv_defs qeq_iffs |
567 qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC |
567 qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC |
568 else [] |
568 else [] |
569 |
569 |
570 |
570 |
571 (* noting the theorems *) |
571 (* noting the theorems *) |