Tue, 24 Jun 2014 08:19:22 +0200 blanchet don't generate Isar proof skeleton for what amounts to a one-line proof
Tue, 24 Jun 2014 08:19:22 +0200 blanchet 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 nipkow r_into_(r)trancl should not be [simp]: helps little and comlicates some AFP proofs
Sat, 21 Jun 2014 15:46:52 +0200 nipkow added [simp]
Sat, 21 Jun 2014 10:41:02 +0200 ballarin Two basic lemmas on bij_betw.
Fri, 20 Jun 2014 09:55:31 +0200 blanchet changed default MaSh parameters based on (in vitro) evaluation
Fri, 20 Jun 2014 09:42:36 +0200 blanchet made 'tptp_graph' more liberal (why reject TFF?)
Wed, 18 Jun 2014 17:42:24 +0200 blanchet made tactic more robust in the face of 'primcorec' specifications containing 'case_sum'
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -8 +8 +10 +30 +100 +300 +1000 +3000 +10000 tip