src/HOL/Tools/BNF/bnf_def_tactics.ML
18 months ago traytel 2017-12-17 made tactics more robust
2016-08-18 traytel 2016-08-18 derive pred_mono property for BNFs
2016-07-05 wenzelm 2016-07-05 more antiquotations;
2016-03-14 blanchet 2016-03-14 strengthened tactics
2016-02-17 traytel 2016-02-17 derive transfer rule for predicator
2016-02-16 traytel 2016-02-16 make predicator a first-class bnf citizen
2015-12-13 wenzelm 2015-12-13 more general types Proof.method / context_tactic; proper context for Method.insert_tac; tuned;
2015-12-01 blanchet 2015-12-01 tuned whitespace
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-09-24 traytel 2015-09-24 congruence rules for the relator
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-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-09-25 desharna 2014-09-25 generate 'rec_transfer' for datatypes
2014-09-01 desharna 2014-09-01 generate 'set_transfer' for BNFs
2014-09-01 desharna 2014-09-01 generate 'rel_transfer' for BNFs
2014-08-18 desharna 2014-08-18 generate 'inj_map_strong' for BNFs
2014-08-18 desharna 2014-08-18 renamed 'rel_mono_strong' to 'rel_mono_strong0'
2014-08-14 desharna 2014-08-14 generate 'rel_map' theorem for BNFs
2014-07-25 blanchet 2014-07-25 tuning
2014-05-08 desharna 2014-05-08 generate 'map_ident' theorem for BNFs
2014-04-23 blanchet 2014-04-23 added 'inj_map' as auxiliary BNF theorem
2014-03-07 wenzelm 2014-03-07 more antiquotations;
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2014-02-21 blanchet 2014-02-21 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-01-31 traytel 2014-01-31 less hermetic tactics
2014-01-29 traytel 2014-01-29 made tactic more robust
2014-01-20 blanchet 2014-01-20 tuned names
2014-01-20 blanchet 2014-01-20 adjusted comments
2014-01-20 blanchet 2014-01-20 avoid nested 'Tools' directories