src/HOL/BNF_FP_Base.thy
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-07-07 desharna 2014-07-07 generate 'rel_cases' theorem for (co)datatypes
2014-07-02 desharna 2014-07-02 generate 'corec_code' theorem for codatatypes
2014-07-01 desharna 2014-07-01 generate 'rel_induct' theorem for datatypes
2014-06-24 desharna 2014-06-24 tune the implementation of 'rel_coinduct'
2014-06-24 desharna 2014-06-24 generate 'rel_coinduct' theorem for codatatypes
2014-06-24 desharna 2014-06-24 generate 'rel_coinduct0' theorem for codatatypes
2014-06-18 blanchet 2014-06-18 made tactic more robust in the face of 'primcorec' specifications containing 'case_sum'
2014-05-04 blanchet 2014-05-04 renamed 'xxx_size' to 'size_xxx' for old datatype package
2014-04-25 blanchet 2014-04-25 more unfolding and more folding in size equations, to look more natural in the nested case
2014-04-23 blanchet 2014-04-23 localize new size function generation code
2014-04-23 blanchet 2014-04-23 no need to make 'size' generation an interpretation -- overkill
2014-04-23 blanchet 2014-04-23 generate 'rec_o_map' and 'size_o_map' in size extension
2014-03-07 blanchet 2014-03-07 balance tuples that represent curried functions
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2014-03-06 traytel 2014-03-06 rationalized imports
2014-03-06 blanchet 2014-03-06 renamed 'map_pair' to 'map_prod'
2014-03-06 blanchet 2014-03-06 renamed 'map_sum' to 'sum_map'
2014-03-06 traytel 2014-03-06 more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms
2014-03-04 blanchet 2014-03-04 simplify sets in BNF composition
2014-03-03 blanchet 2014-03-03 make 'typedef' optional, depending on size of original type
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-23 blanchet 2014-02-23 improved accounting for dead variables when naming set functions (refines d71c2737ee21)
2014-02-23 blanchet 2014-02-23 more precise error message
2014-02-21 blanchet 2014-02-21 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
2014-02-19 blanchet 2014-02-19 moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
2014-02-18 blanchet 2014-02-18 prepare two-stage 'primrec' setup
2014-02-17 blanchet 2014-02-17 tuning * * * moved 'primrec' up to displace the few remaining uses of 'old_primrec'
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-01-20 blanchet 2014-01-20 move BNF_LFP up the dependency chain
2014-01-20 blanchet 2014-01-20 removed dependency of BNF package on Nitpick
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'