src/HOL/Tools/BNF/bnf_fp_n2m.ML
2014-08-06 traytel 2014-08-06 made tactic more robust
2014-07-30 desharna 2014-07-30 generate 'set_induct' theorem for codatatypes
2014-07-07 desharna 2014-07-07 add helper function map_prod
2014-06-27 blanchet 2014-06-27 tuned variable names
2014-06-24 desharna 2014-06-24 tune the implementation of 'rel_coinduct'
2014-04-23 blanchet 2014-04-23 no need to make 'size' generation an interpretation -- overkill
2014-04-23 blanchet 2014-04-23 generate 'rec_o_map' and 'size_o_map' in size extension
2014-04-23 blanchet 2014-04-23 generate size instances for new-style datatypes
2014-04-10 traytel 2014-04-10 use mutual clique information (cf. c451cf8b29c8) to make N2M more robust
2014-04-10 traytel 2014-04-10 made N2M tactic more robust
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-06 blanchet 2014-03-06 renamed 'map_pair' to 'map_prod'
2014-03-06 blanchet 2014-03-06 renamed 'map_sum' to 'sum_map'
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 simplified N2M code now that 'fold' is no longer used by the sugar layer + use right context in all 'force_typ' calls
2014-03-03 blanchet 2014-03-03 rationalized internals
2014-03-03 blanchet 2014-03-03 make 'typedef' optional, depending on size of original type
2014-03-01 traytel 2014-03-01 made SML/NJ happier
2014-02-28 traytel 2014-02-28 made SML/NJ happier
2014-02-25 traytel 2014-02-25 joint work with blanchet: intermediate typedef for the input to fp-operations
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 made SML/NJ happier
2014-02-17 blanchet 2014-02-17 simplified data structure by reducing the incidence of clumsy indices
2014-02-17 blanchet 2014-02-17 renamed 'datatype_new_compat' to 'datatype_compat'
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-14 traytel 2014-02-14 made N2M more robust w.r.t. identical nested types
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