src/HOL/BNF_Def.thy
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'