equal
deleted
inserted
replaced
601 max_new_mono_instances |
601 max_new_mono_instances |
602 (* pseudo-theorem involving the same constants as the subgoal *) |
602 (* pseudo-theorem involving the same constants as the subgoal *) |
603 val subgoal_th = |
603 val subgoal_th = |
604 Logic.list_implies (hyp_ts, concl_t) |
604 Logic.list_implies (hyp_ts, concl_t) |
605 |> Skip_Proof.make_thm thy |
605 |> Skip_Proof.make_thm thy |
|
606 val rths = |
|
607 facts |> chop (length facts div 4) |
|
608 |>> map (pair 1 o snd) |
|
609 ||> map (pair 2 o snd) |
|
610 |> op @ |
|
611 |> cons (0, subgoal_th) |
606 in |
612 in |
607 Monomorph.monomorph atp_schematic_consts_of |
613 Monomorph.monomorph atp_schematic_consts_of rths ctxt |
608 (subgoal_th :: map snd facts |> map (pair 0)) ctxt |
|
609 |> fst |> tl |
614 |> fst |> tl |
610 |> curry ListPair.zip (map fst facts) |
615 |> curry ListPair.zip (map fst facts) |
611 |> maps (fn (name, rths) => map (pair name o snd) rths) |
616 |> maps (fn (name, rths) => map (pair name o snd) rths) |
612 end |
617 end |
613 fun run_slice blacklist (slice, (time_frac, (complete, |
618 fun run_slice blacklist (slice, (time_frac, (complete, |