| #
4778f606 |
|
21-Oct-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Delete trailing whitespace in src/
|
| #
6b2d07ed |
|
02-Jul-2018 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
holyhammer: finalizing port of the translation to SML + adding vampire
|
| #
769e1d6c |
|
30-Jun-2018 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
holyhammer: evaluation of old and new hammer
|
| #
506754eb |
|
27-Jun-2018 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
holyhammer: finishing porting the translation to sml (hh_new function)
|
| #
84da8ccc |
|
11-Jan-2018 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
minimization and prettification shared between tactictoe and holyhammer
|
| #
def93c6c |
|
27-Sep-2017 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
tactictoe: online recording (to be fixed)
|
| #
3124cb7b |
|
19-Sep-2017 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
holyhammer: tactic + pretty-printing
|
| #
024705f6 |
|
12-Sep-2017 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
tactictoe: theorems' features IO + orthogonalization of theorems
|
| #
6ba144e9 |
|
22-Aug-2017 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
holyhammer: removing scripts + tactictoe: wip+ sharing predictors
|
| #
ccaa1d67 |
|
09-Sep-2015 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
holyhammer: refractoring hhReconstruct.sml
|
| #
8fce5d4e |
|
23-Aug-2015 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Reapply 1ab5ef6508
These are necessary for these files to build with Moscow ML.
Please be careful merging changes.
|
| #
9e3aa895 |
|
22-Aug-2015 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
holyHammer update: provers' binaries now needs to be in PATH + working toward incremental export
|
| #
1ab5ef65 |
|
05-Aug-2015 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Get holyhammer to build with Moscow ML.
* It needs to come after metis in the build sequence because it refers
to metisLib.
* Various signatures needed to have 'include Abbrev' added
* Record type inference differs slightly under the two systems; now one
place where it makes a difference has some typing information added
|
| #
99ba6223 |
|
03-Aug-2015 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
holyhammer 1.0
|