src/HOL/BNF_Fixpoint_Base.thy
2016-04-15 traytel 2016-04-15 intermediate definitions and caching in n2m to keep terms small
2016-04-07 traytel 2016-04-07 derive (co)rec uniformly from (un)fold
2016-02-17 blanchet 2016-02-17 making 'pred_inject' a first-class BNF citizen
2016-02-16 traytel 2016-02-16 simp rules for fsts, snds, setl, setr
2016-01-13 blanchet 2016-01-13 generate stronger 'rel_(co)induct' and 'coinduct' principles for mutually (co)recursive (co)datatypes
2015-11-02 blanchet 2015-11-02 don't pollute local theory with needless names
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-08-12 traytel 2015-08-12 new command for lifting BNF structure over typedefs
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-10-21 desharna 2014-10-21 generate 'map_o_corec' for (co)datatypes * * * document 'map_o_corec'
2014-10-21 desharna 2014-10-21 move theorem 'rec_o_map' * * * move documentation of 'rec_o_map'
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-16 blanchet 2014-09-16 register 'prod' and 'sum' as datatypes, to allow N2M through them
2014-09-04 blanchet 2014-09-04 tuned size function generation
2014-09-03 blanchet 2014-09-03 tuning
2014-09-01 blanchet 2014-09-01 renamed BNF theories