equal
deleted
inserted
replaced
370 state |
370 state |
371 |> K () |
371 |> K () |
372 end |
372 end |
373 else if subcommand = minN then |
373 else if subcommand = minN then |
374 let |
374 let |
|
375 val ctxt = ctxt |> Config.put instantiate_inducts false |
375 val i = the_default 1 opt_i |
376 val i = the_default 1 opt_i |
376 val params as {provers, ...} = |
377 val params as {provers, ...} = |
377 get_params Minimize ctxt (("provers", [default_minimize_prover]) :: |
378 get_params Minimize ctxt (("provers", [default_minimize_prover]) :: |
378 override_params) |
379 override_params) |
379 val goal = prop_of (#goal (Proof.goal state)) |
380 val goal = prop_of (#goal (Proof.goal state)) |
401 (("timeout", |
402 (("timeout", |
402 [string_of_real default_learn_atp_timeout]) :: |
403 [string_of_real default_learn_atp_timeout]) :: |
403 override_params @ |
404 override_params @ |
404 [("slice", ["false"]), |
405 [("slice", ["false"]), |
405 ("minimize", ["true"]), |
406 ("minimize", ["true"]), |
406 ("preplay_timeout", ["0"])]))) |
407 ("preplay_timeout", ["0"])])) |
407 (subcommand = learn_atpN orelse subcommand = relearn_atpN) |
408 fact_override (#facts (Proof.goal state)) |
|
409 (subcommand = learn_atpN orelse subcommand = relearn_atpN)) |
408 else if subcommand = kill_learnersN then |
410 else if subcommand = kill_learnersN then |
409 kill_learners () |
411 kill_learners () |
410 else if subcommand = running_learnersN then |
412 else if subcommand = running_learnersN then |
411 running_learners () |
413 running_learners () |
412 else if subcommand = refresh_tptpN then |
414 else if subcommand = refresh_tptpN then |