src/HOL/Library/bnf_lfp_countable.ML
2014-09-11 blanchet 2014-09-11 tuning terminology
2014-09-11 blanchet 2014-09-11 comment
2014-09-08 blanchet 2014-09-08 made new countable tactic work with sorts other than 'type'
2014-09-08 blanchet 2014-09-08 compile
2014-09-03 blanchet 2014-09-03 intelligible errors instead of tactic failures
2014-09-03 blanchet 2014-09-03 made new tactic even more robust
2014-09-03 blanchet 2014-09-03 fixed tactic for n-way mutual recursion, n >= 4 (balanced conjunctions confuse the tactic)
2014-09-03 blanchet 2014-09-03 improved tactic further
2014-09-03 blanchet 2014-09-03 improved new countability tactic
2014-09-03 blanchet 2014-09-03 'prove_sorry' is too dangerous here -- the tactic is sometimes applied to non-theorems
2014-09-03 blanchet 2014-09-03 added compatibility function
2014-09-03 blanchet 2014-09-03 added countable tactic for new-style datatypes