43 fun mk_step_lfs_gfs lfs gfs = |
43 fun mk_step_lfs_gfs lfs gfs = |
44 Prove (qs, xs, l, t, subproofs, sort_facts (lfs, gfs), meths, comment) |
44 Prove (qs, xs, l, t, subproofs, sort_facts (lfs, gfs), meths, comment) |
45 |
45 |
46 fun minimize_half _ min_facts [] time = (min_facts, time) |
46 fun minimize_half _ min_facts [] time = (min_facts, time) |
47 | minimize_half mk_step min_facts (fact :: facts) time = |
47 | minimize_half mk_step min_facts (fact :: facts) time = |
48 (case preplay_isar_step_for_method ctxt [] (Time.+ (time, slack)) meth |
48 (case preplay_isar_step_for_method ctxt [] (time + slack) meth |
49 (mk_step (min_facts @ facts)) of |
49 (mk_step (min_facts @ facts)) of |
50 Played time' => minimize_half mk_step min_facts facts time' |
50 Played time' => minimize_half mk_step min_facts facts time' |
51 | _ => minimize_half mk_step (fact :: min_facts) facts time) |
51 | _ => minimize_half mk_step (fact :: min_facts) facts time) |
52 |
52 |
53 val (min_lfs, time') = minimize_half (fn lfs => mk_step_lfs_gfs lfs gfs0) [] lfs0 time |
53 val (min_lfs, time') = minimize_half (fn lfs => mk_step_lfs_gfs lfs gfs0) [] lfs0 time |