#
2ef0db2e |
|
10-Jan-2019 |
immler <immler@in.tum.de> |
Uref.uref -> Uref.new
|
#
b4bc28b4 |
|
10-Jan-2019 |
immler <immler@in.tum.de> |
introduce Uref for both polyml and mosml
|
#
b1ca9521 |
|
10-Sep-2018 |
Fabian Immler <immler@in.tum.de> |
make heavily allocated variables explicit as local program variables
|
#
499ad7b5 |
|
03-Sep-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Label assignments (v := e) as (* OK *) in src/metis These labels are my judgement that the references are strictly local and so not a concurrency issue. Additionally, some assignments in comments (to Moscow ML specific quietdec, for example) have just been deleted.
|
#
20bbfd8d |
|
31-Aug-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Clean up some METIS library syntax (semantically a no-op) Mostly deleting redundant infix declarations, but some other random reformatting along the way
|
#
838f97d0 |
|
19-Mar-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Up to core types
|
#
82c76808 |
|
21-Jan-2004 |
Joe Hurd <joe@gilith.com> |
* Implemented a HOL specific finite model, which knows about numbers, lists and sets. * Removed multiple provers: METIS_TAC is now solely based on ordered resolution.
|
#
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.
|
#
91bf4ed0 |
|
17-Jun-2003 |
Joe Hurd <joe@gilith.com> |
Version 1.3: 17 June 2002 Goals submitted to MESON_TAC when HOL is built .......... 1953 Proved by MESON_TAC ..................................... 1953 Proved by METIS_TAC within 10s .......................... 1946 Between Versions 1.2 and 1.3 * Implemention of definitional CNF to reduce blow-up in number of clauses (usually caused by nested boolean equivalences). * Resolution is more robust and efficient, and includes an option (off by default) for clauses to inherit ordering constraints.
|
#
01d2e53d |
|
18-Jul-2002 |
Joe Hurd <joe@gilith.com> |
Initial check-in of the Metis first-order prover.
|