| #
10308a8e |
|
31-Aug-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Isolate assignment to traces ref in metis code
Hide assignment to this reference behind add_trace and set_traces
function calls.
|
| #
e6f1d9ff |
|
15-Jan-2005 |
Joe Hurd <joe@gilith.com> |
Improvements to Metis made while investigating bad performance reported
by Anthony, Juliano and Mike.
|
| #
706836b9 |
|
14-Jan-2004 |
Joe Hurd <joe@gilith.com> |
Latest version of METIS_TAC.
The biggest change is that scheduling provers is done by number of
inferences, not time used, so METIS_TAC is now completely
deterministic. If it works for you on a subgoal, it will work every
time HOL4 is built.
|
| #
20ad9a14 |
|
28-Jul-2003 |
Joe Hurd <joe@gilith.com> |
Fixed a bug found by Michael Norrish whereby definitional CNF interacted
badly with type reconstruction. This resulted in some invocations of
METIS_TAC returning "error during proof translation", and then failing to
find a proof with types switched on. All fixed now.
Now that STRIP_TAC has changed, METIS_TAC can safely do pre-normalization
splitting using DISJ_CASES_THEN. The only user-visible result of this
should be better performance.
|
| #
5d643e5d |
|
27-Jun-2003 |
Joe Hurd <joe@gilith.com> |
Fixed a bug discovered by Konrad, where the new version of metis couldn't
prove something the previous version could.
|