equal
deleted
inserted
replaced
40 (if blocking then |
40 (if blocking then |
41 "" |
41 "" |
42 else |
42 else |
43 "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))) |
43 "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))) |
44 |
44 |
45 val auto_minimization_threshold = Unsynchronized.ref 50 |
45 val auto_minimization_threshold = Unsynchronized.ref (!binary_threshold) |
46 |
46 |
47 fun get_minimizing_prover ctxt auto name (params as {debug, verbose, ...}) |
47 fun get_minimizing_prover ctxt auto name (params as {debug, verbose, ...}) |
48 minimize_command |
48 minimize_command |
49 (problem as {state, subgoal, subgoal_count, facts, ...}) = |
49 (problem as {state, subgoal, subgoal_count, facts, ...}) = |
50 get_prover ctxt auto name params minimize_command problem |
50 get_prover ctxt auto name params minimize_command problem |