equal
deleted
inserted
replaced
370 fact_override (minimize_command override_params i) |
370 fact_override (minimize_command override_params i) |
371 state |
371 state |
372 |> K () |
372 |> K () |
373 end |
373 end |
374 else if subcommand = minN then |
374 else if subcommand = minN then |
375 run_minimize (get_params Minimize ctxt |
375 let |
376 (("provers", [default_minimize_prover]) :: |
376 val i = the_default 1 opt_i |
377 override_params)) |
377 val params as {provers, ...} = |
378 (K ()) (the_default 1 opt_i) (#add fact_override) state |
378 get_params Minimize ctxt (("provers", [default_minimize_prover]) :: |
|
379 override_params) |
|
380 val goal = prop_of (#goal (Proof.goal state)) |
|
381 val facts = nearly_all_facts ctxt false fact_override Symtab.empty |
|
382 Termtab.empty [] [] goal |
|
383 val do_learn = mash_learn_proof ctxt params (hd provers) goal facts |
|
384 in run_minimize params do_learn i (#add fact_override) state end |
379 else if subcommand = messagesN then |
385 else if subcommand = messagesN then |
380 messages opt_i |
386 messages opt_i |
381 else if subcommand = supported_proversN then |
387 else if subcommand = supported_proversN then |
382 supported_provers ctxt |
388 supported_provers ctxt |
383 else if subcommand = kill_proversN then |
389 else if subcommand = kill_proversN then |
387 else if subcommand = unlearnN then |
393 else if subcommand = unlearnN then |
388 mash_unlearn ctxt |
394 mash_unlearn ctxt |
389 else if subcommand = learnN orelse subcommand = relearnN then |
395 else if subcommand = learnN orelse subcommand = relearnN then |
390 (if subcommand = relearnN then mash_unlearn ctxt else (); |
396 (if subcommand = relearnN then mash_unlearn ctxt else (); |
391 mash_learn ctxt (get_params Normal ctxt |
397 mash_learn ctxt (get_params Normal ctxt |
392 (("verbose", ["true"]) :: override_params))) |
398 (override_params @ [("verbose", ["true"])]))) |
393 else if subcommand = kill_learnersN then |
399 else if subcommand = kill_learnersN then |
394 kill_learners () |
400 kill_learners () |
395 else if subcommand = running_learnersN then |
401 else if subcommand = running_learnersN then |
396 running_learners () |
402 running_learners () |
397 else if subcommand = refresh_tptpN then |
403 else if subcommand = refresh_tptpN then |