src/HOL/Codatatype/Tools/bnf_gfp.ML
2012-09-08 blanchet 2012-09-08 some work on coiter tactic
2012-09-08 blanchet 2012-09-08 implemented "mk_iter_or_rec_tac"
2012-09-06 traytel 2012-09-06 respect order of/additional type variables supplied by the user in fixed point constructions;
2012-09-06 blanchet 2012-09-06 construct high-level iterator RHS
2012-09-05 blanchet 2012-09-05 honor mixfix specifications
2012-09-04 blanchet 2012-09-04 optionally provide extra dead variables to the FP constructions
2012-09-04 blanchet 2012-09-04 renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix
2012-09-04 blanchet 2012-09-04 implemented "mk_inject_tac"
2012-09-04 blanchet 2012-09-04 implemented "mk_exhaust_tac"
2012-09-04 blanchet 2012-09-04 more work on FP sugar
2012-09-04 blanchet 2012-09-04 more work on sugar + simplify Trueprop + eq idiom everywhere
2012-09-04 blanchet 2012-09-04 more work on FP sugar
2012-09-04 traytel 2012-09-04 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
2012-09-03 traytel 2012-09-03 killed internal output
2012-09-03 traytel 2012-09-03 generate coinductive witnesses for codatatypes
2012-09-03 blanchet 2012-09-03 renamed three BNF/(co)datatype-related commands
2012-08-30 blanchet 2012-08-30 generate "disc_exhaust" property
2012-08-30 blanchet 2012-08-30 renamed ML function for consistency
2012-08-28 blanchet 2012-08-28 added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)