src/HOL/BNF_LFP.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-03 desharna 2014-07-03 generate 'rel_intros' theorem for (co)datatypes
2014-07-01 desharna 2014-07-01 generate 'rel_induct' theorem for datatypes
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 prevent tactic failures by detecting and ignoring BNFs with no 'size' functions early
2014-04-23 blanchet 2014-04-23 move size hooks together, with new one preceding old one and sharing same theory data
2014-04-23 blanchet 2014-04-23 allow registration of custom size functions for BNF-based datatypes
2014-04-23 blanchet 2014-04-23 reverted rb458558cbcc2 -- better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the low-level recursor) and 'rec'
2014-04-23 blanchet 2014-04-23 generate 'rec_o_map' and 'size_o_map' in size extension
2014-04-23 blanchet 2014-04-23 made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
2014-04-23 blanchet 2014-04-23 generate size instances for new-style datatypes
2014-04-01 blanchet 2014-04-01 added BNF interpretation hook
2014-03-21 traytel 2014-03-21 simplified internal datatype construction
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2014-03-03 blanchet 2014-03-03 rationalized internals
2014-03-03 blanchet 2014-03-03 rationalized internals
2014-03-03 blanchet 2014-03-03 rationalized internals
2014-03-03 blanchet 2014-03-03 rationalize internals
2014-03-03 blanchet 2014-03-03 optimized simple non-recursive datatypes by reusing 'case' for 'rec' constant
2014-03-03 blanchet 2014-03-03 got rid of automatically generated fold constant and theorems (to reduce overhead)
2014-03-03 blanchet 2014-03-03 optimize cardinal bounds involving natLeq (omega)
2014-02-28 traytel 2014-02-28 load Metis a little later
2014-02-26 traytel 2014-02-26 intermediate typedef for the type of the bound (local to lfp)
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-17 blanchet 2014-02-17 renamed old 'primrec' to 'old_primrec' (until the new 'primrec' can be moved above 'Nat' in the theory dependencies)
2014-02-17 blanchet 2014-02-17 renamed 'datatype_new_compat' to 'datatype_compat'
2014-02-17 blanchet 2014-02-17 renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
2014-01-20 blanchet 2014-01-20 rationalized lemmas
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'