src/HOL/Tools/BNF/bnf_gfp_tactics.ML
2014-03-22 haftmann 2014-03-22 generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
2014-03-17 traytel 2014-03-17 tuned internal construction
2014-03-13 traytel 2014-03-13 tuned tactics
2014-03-13 traytel 2014-03-13 simplified internal codatatype construction
2014-03-10 traytel 2014-03-10 tuned tactic
2014-03-07 wenzelm 2014-03-07 more antiquotations;
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2014-03-04 blanchet 2014-03-04 renamed a pair of low-level theorems to have c/dtor in their names (like the others)
2014-02-21 traytel 2014-02-21 only one internal coinduction rule
2014-02-21 blanchet 2014-02-21 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
2014-02-20 traytel 2014-02-20 tuned tactic
2014-02-20 traytel 2014-02-20 made tactics more robust
2014-02-19 traytel 2014-02-19 another simplification of internal codatatype construction
2014-02-19 traytel 2014-02-19 simplifications of internal codatatype construction
2014-02-18 traytel 2014-02-18 syntactic simplifications of internal (co)datatype constructions
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-02-12 blanchet 2014-02-12 se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors * * * cleaner simp/iff sets
2014-01-31 traytel 2014-01-31 less hermetic tactics
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