src/HOL/Tools/BNF/bnf_fp_util.ML
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 rationalized internals
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-25 traytel 2014-02-25 joint work with blanchet: intermediate typedef for the input to fp-operations
2014-02-24 blanchet 2014-02-24 added BNF cache (within one definition)
2014-02-23 blanchet 2014-02-23 optimization of 'bnf_of_typ' if all variables are dead
2014-02-23 blanchet 2014-02-23 added explicit killing
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 tuning
2014-02-14 blanchet 2014-02-14 generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
2014-02-14 blanchet 2014-02-14 better handling of recursion through functions
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-02-12 blanchet 2014-02-12 more liberal merging of BNFs and constructor sugar * * * make sure that the cache doesn't produce 'DUP's
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