src/HOL/BNF_Least_Fixpoint.thy
2014-09-11 blanchet 2014-09-11 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
2014-09-09 blanchet 2014-09-09 removed debugging junk
2014-09-09 blanchet 2014-09-09 renamed ML file and module
2014-09-09 blanchet 2014-09-09 made datatype realizer plugin work for new-style datatypes with no nesting
2014-09-08 blanchet 2014-09-08 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
2014-09-04 blanchet 2014-09-04 tweaked setup for datatype realizer
2014-09-04 blanchet 2014-09-04 tuned size function generation
2014-09-03 blanchet 2014-09-03 tuning
2014-09-03 blanchet 2014-09-03 more compatibility functions
2014-09-02 blanchet 2014-09-02 tuning
2014-09-01 blanchet 2014-09-01 renamed BNF theories