equal
deleted
inserted
replaced
600 ((nth pps (kk - 1), find_index (curry (op =) pprem) (nth buckets (kk - 1)) + 1), |
600 ((nth pps (kk - 1), find_index (curry (op =) pprem) (nth buckets (kk - 1)) + 1), |
601 (length xysets, kk))) pprems |
601 (length xysets, kk))) pprems |
602 end; |
602 end; |
603 |
603 |
604 val ppjjqqkksss = map (map (mk_raw_prem_prems_indices o #2)) raw_premss; |
604 val ppjjqqkksss = map (map (mk_raw_prem_prems_indices o #2)) raw_premss; |
|
605 val _ = tracing ("val ppjjqqkksss = " ^ PolyML.makestring ppjjqqkksss) (*###*) |
605 |
606 |
606 val fld_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss); |
607 val fld_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss); |
607 |
608 |
608 val induct_thm = |
609 val induct_thm = |
609 Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => |
610 Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => |