src/HOL/Codatatype/BNF_Comp.thy
2012-09-12 blanchet 2012-09-12 moved theorems closer to where they are used
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-08-30 blanchet 2012-08-30 killed obsolete "bnf_of_typ" command
2012-08-28 blanchet 2012-08-28 added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)