src/HOL/Codatatype/Tools/bnf_gfp_util.ML
2012-09-11 blanchet 2012-09-11 split sum types in corecursor definition
2012-09-04 blanchet 2012-09-04 implemented "mk_case_tac" -- and got rid of "cheat_tac"
2012-09-04 blanchet 2012-09-04 define "case" constant
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 FP sugar
2012-08-30 blanchet 2012-08-30 more work on BNF sugar -- up to derivation of nchotomy
2012-08-28 blanchet 2012-08-28 added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)