Tue, 24 Jun 2014 13:48:14 +0200 generate 'rel_coinduct' theorem for codatatypes
desharna [Tue, 24 Jun 2014 13:48:14 +0200] rev 57302
generate 'rel_coinduct' theorem for codatatypes
Tue, 24 Jun 2014 13:48:14 +0200 generate 'rel_coinduct0' theorem for codatatypes
desharna [Tue, 24 Jun 2014 13:48:14 +0200] rev 57301
generate 'rel_coinduct0' theorem for codatatypes
Tue, 24 Jun 2014 12:36:45 +0200 added parentheses around type arguments in THF
blanchet [Tue, 24 Jun 2014 12:36:45 +0200] rev 57300
added parentheses around type arguments in THF
Tue, 24 Jun 2014 12:36:45 +0200 optimize log
blanchet [Tue, 24 Jun 2014 12:36:45 +0200] rev 57299
optimize log
Tue, 24 Jun 2014 12:35:57 +0200 enable TF-IDF
blanchet [Tue, 24 Jun 2014 12:35:57 +0200] rev 57298
enable TF-IDF
Tue, 24 Jun 2014 12:35:49 +0200 added another experimental engine
blanchet [Tue, 24 Jun 2014 12:35:49 +0200] rev 57297
added another experimental engine
Tue, 24 Jun 2014 12:35:43 +0200 tweaked experimental setup
blanchet [Tue, 24 Jun 2014 12:35:43 +0200] rev 57296
tweaked experimental setup
Tue, 24 Jun 2014 08:20:00 +0200 changed order of facts so that 'name_tabs' has the same order everywhere (which affects unaliasing)
blanchet [Tue, 24 Jun 2014 08:20:00 +0200] rev 57295
changed order of facts so that 'name_tabs' has the same order everywhere (which affects unaliasing)
Tue, 24 Jun 2014 08:19:58 +0200 use strings to communicate with external process, to ease debugging
blanchet [Tue, 24 Jun 2014 08:19:58 +0200] rev 57294
use strings to communicate with external process, to ease debugging
Tue, 24 Jun 2014 08:19:57 +0200 added 'dummy_thf_ml' prover for experiments with HOLyHammer
blanchet [Tue, 24 Jun 2014 08:19:57 +0200] rev 57293
added 'dummy_thf_ml' prover for experiments with HOLyHammer
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip