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
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip