src/HOL/Codatatype/Tools/bnf_util.ML
2012-09-10 blanchet 2012-09-10 use balanced sums for constructors (to gracefully handle 100 constructors or more)
2012-09-09 traytel 2012-09-09 open typedefs everywhere in the package
2012-09-08 blanchet 2012-09-08 more sugar on codatatypes
2012-09-08 blanchet 2012-09-08 define coiterators
2012-09-08 blanchet 2012-09-08 correctly curry recursor arguments
2012-09-06 blanchet 2012-09-06 tuning
2012-09-06 blanchet 2012-09-06 introduced and used "mk_Freesss", and simplified "mk_Freess(')"
2012-09-06 blanchet 2012-09-06 construct high-level iterator RHS
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-03 blanchet 2012-09-03 rearrange dependencies
2012-08-28 blanchet 2012-08-28 added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)