Tue, 24 Jun 2014 13:48:14 +0200 document property 'rel_coinduct'
desharna [Tue, 24 Jun 2014 13:48:14 +0200] rev 57304
document property 'rel_coinduct'
Tue, 24 Jun 2014 13:48:14 +0200 tune the implementation of 'rel_coinduct'
desharna [Tue, 24 Jun 2014 13:48:14 +0200] rev 57303
tune the implementation of 'rel_coinduct'
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
Tue, 24 Jun 2014 08:19:56 +0200 phantoms may also occur in THF1
blanchet [Tue, 24 Jun 2014 08:19:56 +0200] rev 57292
phantoms may also occur in THF1
Tue, 24 Jun 2014 08:19:55 +0200 added experimental MaSh engine
blanchet [Tue, 24 Jun 2014 08:19:55 +0200] rev 57291
added experimental MaSh engine
Tue, 24 Jun 2014 08:19:55 +0200 move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet [Tue, 24 Jun 2014 08:19:55 +0200] rev 57290
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
Tue, 24 Jun 2014 08:19:54 +0200 help reconstruction of Z3 skolemization by weakening formulas a bit
blanchet [Tue, 24 Jun 2014 08:19:54 +0200] rev 57289
help reconstruction of Z3 skolemization by weakening formulas a bit
Tue, 24 Jun 2014 08:19:22 +0200 supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet [Tue, 24 Jun 2014 08:19:22 +0200] rev 57288
supports gradual skolemization (cf. Z3) by threading context through correctly
Tue, 24 Jun 2014 08:19:22 +0200 given two one-liners, only show the best of the two
blanchet [Tue, 24 Jun 2014 08:19:22 +0200] rev 57287
given two one-liners, only show the best of the two
Tue, 24 Jun 2014 08:19:22 +0200 don't generate Isar proof skeleton for what amounts to a one-line proof
blanchet [Tue, 24 Jun 2014 08:19:22 +0200] rev 57286
don't generate Isar proof skeleton for what amounts to a one-line proof
Tue, 24 Jun 2014 08:19:22 +0200 don't accidentally transform 'show' into 'obtains' (in general, more 'obtain's could be turned into 'have's, but this is not necessary for the correctness of the proof)
blanchet [Tue, 24 Jun 2014 08:19:22 +0200] rev 57285
don't accidentally transform 'show' into 'obtains' (in general, more 'obtain's could be turned into 'have's, but this is not necessary for the correctness of the proof)
Sun, 22 Jun 2014 12:37:55 +0200 r_into_(r)trancl should not be [simp]: helps little and comlicates some AFP proofs
nipkow [Sun, 22 Jun 2014 12:37:55 +0200] rev 57284
r_into_(r)trancl should not be [simp]: helps little and comlicates some AFP proofs
Sat, 21 Jun 2014 15:46:52 +0200 added [simp]
nipkow [Sat, 21 Jun 2014 15:46:52 +0200] rev 57283
added [simp]
Sat, 21 Jun 2014 10:41:02 +0200 Two basic lemmas on bij_betw.
ballarin [Sat, 21 Jun 2014 10:41:02 +0200] rev 57282
Two basic lemmas on bij_betw.
Fri, 20 Jun 2014 09:55:31 +0200 changed default MaSh parameters based on (in vitro) evaluation
blanchet [Fri, 20 Jun 2014 09:55:31 +0200] rev 57281
changed default MaSh parameters based on (in vitro) evaluation
Fri, 20 Jun 2014 09:42:36 +0200 made 'tptp_graph' more liberal (why reject TFF?)
blanchet [Fri, 20 Jun 2014 09:42:36 +0200] rev 57280
made 'tptp_graph' more liberal (why reject TFF?)
Wed, 18 Jun 2014 17:42:24 +0200 made tactic more robust in the face of 'primcorec' specifications containing 'case_sum'
blanchet [Wed, 18 Jun 2014 17:42:24 +0200] rev 57279
made tactic more robust in the face of 'primcorec' specifications containing 'case_sum'
Wed, 18 Jun 2014 17:42:24 +0200 more MaSh engine variations, for evaluations
blanchet [Wed, 18 Jun 2014 17:42:24 +0200] rev 57278
more MaSh engine variations, for evaluations
Wed, 18 Jun 2014 17:42:24 +0200 split parameter into two
blanchet [Wed, 18 Jun 2014 17:42:24 +0200] rev 57277
split parameter into two
Wed, 18 Jun 2014 14:31:32 +0200 filters are easier to define with INF on filters.
hoelzl [Wed, 18 Jun 2014 14:31:32 +0200] rev 57276
filters are easier to define with INF on filters.
Wed, 18 Jun 2014 07:31:12 +0200 moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl [Wed, 18 Jun 2014 07:31:12 +0200] rev 57275
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 tip