src/HOL/Tools/BNF/bnf_lfp.ML
2014-04-23 blanchet 2014-04-23 generate size instances for new-style datatypes
2014-04-10 traytel 2014-04-10 more accurate type arguments for intermeadiate typedefs
2014-04-01 traytel 2014-04-01 more precise BNF bound for datatypes
2014-04-01 blanchet 2014-04-01 tuning
2014-04-01 blanchet 2014-04-01 added BNF interpretation hook
2014-04-01 traytel 2014-04-01 tuned
2014-03-25 traytel 2014-03-25 prove theorems with fixed variables (export afterwards)
2014-03-24 traytel 2014-03-24 made tactic more robust
2014-03-21 traytel 2014-03-21 simplified internal datatype construction
2014-03-18 traytel 2014-03-18 changed policy when to define constants
2014-03-13 traytel 2014-03-13 tuned tactics
2014-03-10 traytel 2014-03-10 unfold intermediate definitions after sealing the bnf
2014-03-04 blanchet 2014-03-04 renamed a pair of low-level theorems to have c/dtor in their names (like the others)
2014-03-04 traytel 2014-03-04 N2M does not use the low-level 'fold'; removed the latter from the fp_result interface;
2014-03-03 blanchet 2014-03-03 rationalized internals
2014-03-03 blanchet 2014-03-03 optimize cardinal bounds involving natLeq (omega)
2014-02-25 traytel 2014-02-25 joint work with blanchet: intermediate typedef for the input to fp-operations
2014-02-26 traytel 2014-02-26 intermediate typedef for the type of the bound (local to lfp)
2014-02-26 traytel 2014-02-26 made tactics more robust
2014-02-23 blanchet 2014-02-23 improved accounting for dead variables when naming set functions (refines d71c2737ee21)
2014-02-18 traytel 2014-02-18 syntactic simplifications of internal (co)datatype constructions
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 tuning: moved code where it belongs
2014-02-14 traytel 2014-02-14 register bnfs for (co)datatypes under their proper name (lost in af71b753c459)
2014-01-31 traytel 2014-01-31 use Local_Theory.define instead of Specification.definition for internal constants
2014-01-31 traytel 2014-01-31 less hermetic tactics
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