| #
00240c4d |
|
21-Jul-2018 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
share code between tacticToe and holyHammer + start exp with conjecturing
|
| #
2b238455 |
|
07-Mar-2018 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
remove trailing white spaces
|
| #
9a34c699 |
|
12-Jan-2018 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
holyhammer: adding namespace thms
|
| #
a3eea26c |
|
15-Dec-2017 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
holyhammer: stateless writer + before removing external predictors
|
| #
5bc09715 |
|
28-Nov-2017 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
tactictoe: monte carlo wip
|
| #
8c60d4f0 |
|
17-Oct-2017 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
holyhammer: exporting theories by adding a filter on write_thyl
|
| #
6ba144e9 |
|
22-Aug-2017 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
holyhammer: removing scripts + tactictoe: wip+ sharing predictors
|
| #
79ae21ed |
|
07-Nov-2015 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
Fix a potential bug the proof contains a constant named file
|
| #
9a512186 |
|
09-Sep-2015 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
holyhammer: cleaning up experiments
|
| #
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
|