src/HOL/Codatatype/Codatatype.thy
2012-09-12 blanchet 2012-09-12 split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
2012-09-12 blanchet 2012-09-12 reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping
2012-09-11 blanchet 2012-09-11 added "defaults" option
2012-09-11 blanchet 2012-09-11 move "bnf_util.ML" to "BNF_Util.thy"
2012-09-04 blanchet 2012-09-04 more work on sugar + simplify Trueprop + eq idiom everywhere
2012-09-04 blanchet 2012-09-04 started work on sugared "(co)data" commands
2012-09-03 blanchet 2012-09-03 rearrange dependencies
2012-09-03 blanchet 2012-09-03 renamed three BNF/(co)datatype-related commands
2012-08-30 blanchet 2012-08-30 more work on BNF sugar -- up to derivation of nchotomy
2012-08-30 blanchet 2012-08-30 started work on datatype sugar
2012-08-28 blanchet 2012-08-28 added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)