#
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
|