src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
2014-03-22 wenzelm 2014-03-22 more antiquotations;
2014-03-14 panny 2014-03-14 print warning if some constructors are missing; make this warning optional via "(nonexhaustive)"
2014-03-03 blanchet 2014-03-03 rationalized internals
2014-02-27 blanchet 2014-02-27 correct most general type for mutual recursion when several identical types are involved
2014-02-19 blanchet 2014-02-19 adapted Nitpick to 'primrec' refactoring
2014-02-19 blanchet 2014-02-19 moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
2014-02-19 blanchet 2014-02-19 rewrote a small portion of code to avoid dependency on low-level constant
2014-02-19 blanchet 2014-02-19 tuning
2014-02-18 blanchet 2014-02-18 prepare two-stage 'primrec' setup
2014-02-18 blanchet 2014-02-18 tuning
2014-02-17 blanchet 2014-02-17 simplified data structure by reducing the incidence of clumsy indices
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 name derivations in 'primrec' for code extraction from proof terms
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-02-17 blanchet 2014-02-17 tuning: moved code where it belongs
2014-02-17 blanchet 2014-02-17 have 'primrec_new' fall back on old 'primrec' when given old-style datatypes
2014-02-17 blanchet 2014-02-17 tuning
2014-02-14 blanchet 2014-02-14 removed assumption in 'primrec_new' that a given constructor can only occur once
2014-02-14 blanchet 2014-02-14 allow different functions to recurse on the same type, like in the old package
2014-02-14 blanchet 2014-02-14 have 'Ctr_Sugar' register its 'Spec_Rules'
2014-01-20 blanchet 2014-01-20 tuned names
2014-01-20 blanchet 2014-01-20 adjusted comments
2014-01-20 blanchet 2014-01-20 avoid nested 'Tools' directories