src/HOL/Codatatype/Tools/bnf_gfp.ML
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)