Wed, 03 Sep 2014 22:47:05 +0200 blanchet reenabled example
Wed, 03 Sep 2014 22:47:05 +0200 blanchet improved new countability tactic
Wed, 03 Sep 2014 22:47:05 +0200 blanchet 'prove_sorry' is too dangerous here -- the tactic is sometimes applied to non-theorems
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 tip