src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
Tue, 09 Sep 2014 23:54:39 +0200 blanchet proper checks -- the calls data structure may contain spurious entries
Tue, 09 Sep 2014 20:51:36 +0200 blanchet more canonical (and correct) local theory threading
Mon, 08 Sep 2014 19:21:19 +0200 blanchet made N2M work with sort constraints (cf. TODO)
Mon, 08 Sep 2014 19:21:07 +0200 blanchet honour sorts in N2M
Mon, 08 Sep 2014 14:03:35 +0200 blanchet improved caching
Mon, 08 Sep 2014 14:03:01 +0200 blanchet extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
Thu, 04 Sep 2014 09:02:43 +0200 blanchet moved code around
Thu, 04 Sep 2014 09:02:43 +0200 blanchet tuned size function generation
Mon, 01 Sep 2014 19:28:00 +0200 blanchet drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
Mon, 01 Sep 2014 16:17:47 +0200 blanchet more compatibility between old- and new-style datatypes
Mon, 01 Sep 2014 16:17:47 +0200 blanchet made transfer functions slightly more general
Mon, 01 Sep 2014 16:17:46 +0200 blanchet renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
Mon, 18 Aug 2014 17:19:58 +0200 blanchet reordered some (co)datatype property names for more consistency
Tue, 12 Aug 2014 15:48:59 +0200 blanchet improved unfolding of 'let's
Tue, 12 Aug 2014 15:48:59 +0200 blanchet less aggressive unfolding; removed debugging;
Wed, 02 Jul 2014 17:01:49 +0200 desharna generate 'corec_code' theorem for codatatypes
Fri, 27 Jun 2014 10:11:44 +0200 blanchet tuned variable names
Wed, 23 Apr 2014 10:23:27 +0200 blanchet no need to make 'size' generation an interpretation -- overkill
Wed, 23 Apr 2014 10:23:27 +0200 blanchet manual merge + added 'rel_distincts' field to record for symmetry
Wed, 23 Apr 2014 10:23:26 +0200 blanchet reverted rb458558cbcc2 -- better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the low-level recursor) and 'rec'
Wed, 23 Apr 2014 10:23:26 +0200 blanchet generate size instances for new-style datatypes
Thu, 10 Apr 2014 17:48:16 +0200 kuncar export theorems
Wed, 09 Apr 2014 18:40:21 +0200 blanchet generate cliques for 'prim(co)rec' N2M
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
Mon, 03 Mar 2014 12:48:20 +0100 blanchet rationalized internals
Mon, 03 Mar 2014 12:48:20 +0100 blanchet rationalized internals
Mon, 03 Mar 2014 12:48:20 +0100 blanchet rationalized internals
Mon, 03 Mar 2014 12:48:20 +0100 blanchet rationalize internals
Mon, 03 Mar 2014 12:48:20 +0100 blanchet optimized simple non-recursive datatypes by reusing 'case' for 'rec' constant
Mon, 03 Mar 2014 12:48:20 +0100 blanchet got rid of automatically generated fold constant and theorems (to reduce overhead)
Tue, 25 Feb 2014 18:14:26 +0100 traytel joint work with blanchet: intermediate typedef for the input to fp-operations
Thu, 27 Feb 2014 13:04:57 +0100 blanchet correct most general type for mutual recursion when several identical types are involved
Sun, 23 Feb 2014 22:51:11 +0100 blanchet improved accounting for dead variables when naming set functions (refines d71c2737ee21)
Sun, 23 Feb 2014 22:51:11 +0100 blanchet added explicit killing
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:28 +0100 blanchet tuning
Mon, 17 Feb 2014 22:54:38 +0100 blanchet simplified data structure by reducing the incidence of clumsy indices
Fri, 14 Feb 2014 18:42:43 +0100 blanchet generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
Fri, 14 Feb 2014 15:03:24 +0100 blanchet allow different functions to recurse on the same type, like in the old package
Fri, 14 Feb 2014 15:03:23 +0100 blanchet 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
Wed, 12 Feb 2014 17:36:00 +0100 blanchet 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')
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 made 'ctr_sugar' more friendly to the 'datatype_realizer'
Wed, 12 Feb 2014 08:35:56 +0100 blanchet more liberal merging of BNFs and constructor sugar
Thu, 06 Feb 2014 00:24:02 +0100 blanchet expand 'split' in direct corecursion as well
Wed, 05 Feb 2014 16:33:22 +0100 blanchet fixed handling of 'split'
Tue, 21 Jan 2014 14:52:23 +0100 blanchet made SML/NJ happier
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