src/HOL/Tools/BNF/bnf_gfp.ML
2014-03-10 traytel 2014-03-10 tuned tactic
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-04 blanchet 2014-03-04 removed debugging leftover
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-21 traytel 2014-02-21 only one internal coinduction rule
2014-02-21 blanchet 2014-02-21 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
2014-02-20 traytel 2014-02-20 made tactics more robust
2014-02-19 traytel 2014-02-19 another simplification of internal codatatype construction
2014-02-19 traytel 2014-02-19 simplifications of internal codatatype construction
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-02-12 blanchet 2014-02-12 adapted theories to 'xxx_case' to 'case_xxx' * * * 'char_case' -> 'case_char' and same for 'rec' * * * compile * * * renamed 'xxx_case' to 'case_xxx'
2014-02-12 blanchet 2014-02-12 renamed 'nat_{case,rec}' to '{case,rec}_nat'
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-02-12 blanchet 2014-02-12 adapted theories to '{case,rec}_{list,option}' names
2014-02-12 blanchet 2014-02-12 se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors * * * cleaner simp/iff sets
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 made BNF compile after move to HOL
2014-01-20 blanchet 2014-01-20 adjusted comments
2014-01-20 blanchet 2014-01-20 avoid nested 'Tools' directories