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