| #
08d7a558 |
|
23-Oct-2014 |
Piotr Trojanek <piotr.trojanek@gmail.com> |
trailing newlines in *.{sml,sig} files from src/ removed
Trailing newlines from SML files in src/ were rendered in HTML documentation.
|
| #
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.
|
| #
7850f004 |
|
21-Sep-2002 |
Joe Hurd <joe@gilith.com> |
Version 1.1 of the Metis Library.
From the Change Log section of the README:
Between Versions 1.0 and 1.1
* Added a "metis" entry to the HOL trace system: it nows prints
status information during proof (if HOL is in interactive mode).
* Restricted (universal and existential) quantifiers are now
normalized by the NNF conversion.
* (First-order) METIS_TAC can now handle boolean variables.
* Improved performance in the model elimination proof procedure due
to better caching (following a suggestion from John Harrison).
* First-order substitutions are now fully Boultonized.
* The first-order logical kernel makes local tweaks to keep proofs
as small as possible.
|
| #
01d2e53d |
|
18-Jul-2002 |
Joe Hurd <joe@gilith.com> |
Initial check-in of the Metis first-order prover.
|