src/HOL/BNF_Def.thy
2016-09-11 wenzelm 2016-09-11 tuned proofs;
2016-08-18 traytel 2016-08-18 derive pred_mono property for BNFs
2016-05-13 wenzelm 2016-05-13 eliminated use of empty "assms";
2016-02-17 traytel 2016-02-17 derive transfer rule for predicator
2016-02-16 traytel 2016-02-16 make predicator a first-class bnf citizen
2015-11-15 wenzelm 2015-11-15 option "inductive_defs" controls exposure of def and mono facts;
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-10-13 haftmann 2015-10-13 emphasized general nature of parameter
2015-10-13 haftmann 2015-10-13 moved lemmas
2015-09-24 traytel 2015-09-24 more useful properties of the relators
2015-08-27 haftmann 2015-08-27 standardized some occurences of ancient "split" alias
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-03-16 traytel 2015-03-16 BNF relators preserve reflexivity
2015-02-11 Andreas Lochbihler 2015-02-11 add monotonicity lemmas for rel_fun
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 'rec_transfer' for datatypes
2014-09-16 blanchet 2014-09-16 register 'prod' and 'sum' as datatypes, to allow N2M through them
2014-09-01 desharna 2014-09-01 generate 'set_transfer' for BNFs
2014-09-01 desharna 2014-09-01 generate 'rel_transfer' for BNFs
2014-08-06 traytel 2014-08-06 handle deep nesting in N2M
2014-07-29 blanchet 2014-07-29 header tuning
2014-07-24 wenzelm 2014-07-24 more robust notation BNF_Def.convol, which is private to main HOL, but may cause syntax ambiguities nonetheless (e.g. List.thy);
2014-06-27 blanchet 2014-06-27 merged two small theory files
2014-04-23 blanchet 2014-04-23 added 'inj_map' as auxiliary BNF theorem
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2014-02-28 traytel 2014-02-28 load Metis a little later
2014-02-25 traytel 2014-02-25 joint work with blanchet: intermediate typedef for the input to fp-operations
2014-02-21 blanchet 2014-02-21 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-01-29 traytel 2014-01-29 made tactic more robust
2014-01-20 blanchet 2014-01-20 moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
2014-01-20 blanchet 2014-01-20 tuning
2014-01-20 blanchet 2014-01-20 made BNF compile after move to HOL
2014-01-20 blanchet 2014-01-20 tuned comments
2014-01-20 blanchet 2014-01-20 moved BNF files to 'HOL'