src/HOL/Library/bnf_lfp_countable.ML
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-07-16 traytel 2015-07-16 {r,e,d,f}tac with proper context in BNF
2015-04-08 wenzelm 2015-04-08 proper context for Object_Logic operations;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-10-08 wenzelm 2014-10-08 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
2014-09-26 desharna 2014-09-26 refactor fp_sugar move theorems
2014-09-26 desharna 2014-09-26 refactor fp_sugar move theorems
2014-09-26 desharna 2014-09-26 refactor fp_sugar move theorems
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