src/HOL/Tools/BNF/bnf_lfp.ML
Tue, 18 Mar 2014 14:32:23 +0100 traytel changed policy when to define constants
Thu, 13 Mar 2014 16:28:25 +0100 traytel tuned tactics
Mon, 10 Mar 2014 13:23:16 +0100 traytel unfold intermediate definitions after sealing the bnf
Tue, 04 Mar 2014 18:57:17 +0100 blanchet renamed a pair of low-level theorems to have c/dtor in their names (like the others)
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 12:48:20 +0100 blanchet rationalized internals
Mon, 03 Mar 2014 12:48:19 +0100 blanchet optimize cardinal bounds involving natLeq (omega)
Tue, 25 Feb 2014 18:14:26 +0100 traytel joint work with blanchet: intermediate typedef for the input to fp-operations
Wed, 26 Feb 2014 23:09:29 +0100 traytel intermediate typedef for the type of the bound (local to lfp)
Wed, 26 Feb 2014 10:10:38 +0100 traytel made tactics more robust
Sun, 23 Feb 2014 22:51:11 +0100 blanchet improved accounting for dead variables when naming set functions (refines d71c2737ee21)
Tue, 18 Feb 2014 14:51:26 +0100 traytel syntactic simplifications of internal (co)datatype constructions
Mon, 17 Feb 2014 18:18:27 +0100 blanchet tuning
Mon, 17 Feb 2014 13:31:42 +0100 blanchet tuning: moved code where it belongs
Fri, 14 Feb 2014 13:45:29 +0100 traytel register bnfs for (co)datatypes under their proper name (lost in af71b753c459)
Fri, 31 Jan 2014 12:16:59 +0100 traytel use Local_Theory.define instead of Specification.definition for internal constants
Fri, 31 Jan 2014 10:02:36 +0100 traytel less hermetic tactics
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