src/HOL/Tools/BNF/bnf_fp_n2m.ML
Wed, 23 Apr 2014 10:23:26 +0200 blanchet generate size instances for new-style datatypes
Thu, 10 Apr 2014 10:52:48 +0200 traytel use mutual clique information (cf. c451cf8b29c8) to make N2M more robust
Thu, 10 Apr 2014 09:38:38 +0200 traytel made N2M tactic more robust
Wed, 09 Apr 2014 18:22:11 +0200 blanchet thread mutual cliques through
Fri, 07 Mar 2014 01:02:21 +0100 blanchet balance tuples that represent curried functions
Thu, 06 Mar 2014 13:36:48 +0100 blanchet renamed 'map_pair' to 'map_prod'
Thu, 06 Mar 2014 13:36:15 +0100 blanchet renamed 'map_sum' to 'sum_map'
Tue, 04 Mar 2014 12:32:33 +0100 traytel N2M does not use the low-level 'fold'; removed the latter from the fp_result interface;
Mon, 03 Mar 2014 23:05:49 +0100 blanchet simplified N2M code now that 'fold' is no longer used by the sugar layer + use right context in all 'force_typ' calls
Mon, 03 Mar 2014 12:48:20 +0100 blanchet rationalized internals
Mon, 03 Mar 2014 12:48:20 +0100 blanchet make 'typedef' optional, depending on size of original type
Sat, 01 Mar 2014 20:40:31 +0100 traytel made SML/NJ happier
Fri, 28 Feb 2014 22:00:13 +0100 traytel made SML/NJ happier
Tue, 25 Feb 2014 18:14:26 +0100 traytel joint work with blanchet: intermediate typedef for the input to fp-operations
Wed, 19 Feb 2014 08:34:33 +0100 blanchet moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
Tue, 18 Feb 2014 17:52:27 +0100 blanchet made SML/NJ happier
Mon, 17 Feb 2014 22:54:38 +0100 blanchet simplified data structure by reducing the incidence of clumsy indices
Mon, 17 Feb 2014 13:31:42 +0100 blanchet renamed 'datatype_new_compat' to 'datatype_compat'
Mon, 17 Feb 2014 13:31:42 +0100 blanchet renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
Fri, 14 Feb 2014 14:54:08 +0100 traytel made N2M more robust w.r.t. identical nested types
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed '{prod,sum,bool,unit}_case' to 'case_...'
Wed, 12 Feb 2014 08:35:56 +0100 blanchet more liberal merging of BNFs and constructor sugar
Mon, 20 Jan 2014 18:24:56 +0100 blanchet tuned names
Mon, 20 Jan 2014 18:24:56 +0100 blanchet adjusted comments
Mon, 20 Jan 2014 18:24:56 +0100 blanchet avoid nested 'Tools' directories
less more (0) tip