equal
deleted
inserted
replaced
46 |
46 |
47 val trace = Unsynchronized.ref false; |
47 val trace = Unsynchronized.ref false; |
48 fun trace_msg msg = if ! trace then tracing (msg ()) else (); |
48 fun trace_msg msg = if ! trace then tracing (msg ()) else (); |
49 |
49 |
50 val max_clauses_default = 60; |
50 val max_clauses_default = 60; |
51 val (max_clauses, setup) = Attrib.config_int "max_clauses" (K max_clauses_default); |
51 val (max_clauses, setup) = Attrib.config_int "meson_max_clauses" (K max_clauses_default); |
52 |
52 |
53 (*No known example (on 1-5-2007) needs even thirty*) |
53 (*No known example (on 1-5-2007) needs even thirty*) |
54 val iter_deepen_limit = 50; |
54 val iter_deepen_limit = 50; |
55 |
55 |
56 val disj_forward = @{thm disj_forward}; |
56 val disj_forward = @{thm disj_forward}; |