src/HOL/BNF_Least_Fixpoint.thy
2017-07-20 blanchet 2017-07-20 strengthened tactic
2016-07-29 Andreas Lochbihler 2016-07-29 add lemmas contributed by Peter Gammie
2016-04-07 traytel 2016-04-07 removed duplicate lemma
2016-04-07 traytel 2016-04-07 derive (co)rec uniformly from (un)fold
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2014-11-07 traytel 2014-11-07 more complete fp_sugars for sum and prod; tuned; removed theorem duplicates; removed obsolete Lifting_{Option,Product,Sum} theories
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-25 desharna 2014-09-25 generate 'corec_transfer' for codatatypes
2014-09-25 desharna 2014-09-25 generate 'rec_transfer' for datatypes
2014-09-25 desharna 2014-09-25 generate 'dtor_corec_transfer' for codatatypes
2014-09-25 desharna 2014-09-25 generate 'ctor_rec_transfer' for datatypes
2014-09-18 blanchet 2014-09-18 moved old 'size' generator together with 'old_datatype'
2014-09-18 blanchet 2014-09-18 moved datatype realizer to 'old_datatype' and colleagues
2014-09-16 blanchet 2014-09-16 register 'prod' and 'sum' as datatypes, to allow N2M through them
2014-09-11 blanchet 2014-09-11 compile
2014-09-11 blanchet 2014-09-11 updated news
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