src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
2014-04-23 blanchet 2014-04-23 generate size instances for new-style datatypes
2014-04-10 kuncar 2014-04-10 export theorems
2014-04-09 blanchet 2014-04-09 generate cliques for 'prim(co)rec' N2M
2014-04-09 blanchet 2014-04-09 thread mutual cliques through
2014-03-07 blanchet 2014-03-07 balance tuples that represent curried functions
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-02-25 traytel 2014-02-25 joint work with blanchet: intermediate typedef for the input to fp-operations
2014-02-27 blanchet 2014-02-27 correct most general type for mutual recursion when several identical types are involved
2014-02-23 blanchet 2014-02-23 improved accounting for dead variables when naming set functions (refines d71c2737ee21)
2014-02-23 blanchet 2014-02-23 added explicit killing
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-17 blanchet 2014-02-17 simplified data structure by reducing the incidence of clumsy indices
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 allow different functions to recurse on the same type, like in the old package
2014-02-14 blanchet 2014-02-14 improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
2014-02-12 blanchet 2014-02-12 iteration n in the 'default' vs. 'update_new' vs. 'update' saga -- 'update' makes sense now that we honor the canonical order on 'merge' (as opposed to raising 'DUP')
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-02-12 blanchet 2014-02-12 made 'ctr_sugar' more friendly to the 'datatype_realizer' * * * reverted changes to 'datatype_realizer.ML'
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-02-06 blanchet 2014-02-06 expand 'split' in direct corecursion as well
2014-02-05 blanchet 2014-02-05 fixed handling of 'split'
2014-01-21 blanchet 2014-01-21 made SML/NJ happier
2014-01-20 blanchet 2014-01-20 adjusted comments
2014-01-20 blanchet 2014-01-20 avoid nested 'Tools' directories