src/HOL/Library/bnf_lfp_countable.ML
Wed, 03 Sep 2014 22:47:05 +0200 blanchet improved tactic further
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
Wed, 03 Sep 2014 09:43:00 +0200 blanchet added compatibility function
Wed, 03 Sep 2014 00:31:38 +0200 blanchet added countable tactic for new-style datatypes
less more (0) tip