src/HOL/Tools/ctr_sugar.ML
Thu, 05 Dec 2013 14:35:58 +0100 blanchet proper code generation for discriminators/selectors
Thu, 05 Dec 2013 14:11:45 +0100 blanchet reverted 141cb34744de and e78e7df36690 -- better provide nicer "eta-expanded" definitions for discriminators and selectors, since users might want to unfold them
Mon, 02 Dec 2013 20:31:54 +0100 blanchet added 'no_code' option
Mon, 02 Dec 2013 20:31:54 +0100 blanchet repaired inconsistency introduced in transiting to 'Local_Theory.define'
Mon, 02 Dec 2013 20:31:54 +0100 blanchet avoid user-level 'Specification.definition' for internal constructions (to avoid e.g. automatic code generation behavior)
Mon, 02 Dec 2013 20:31:54 +0100 blanchet don't try to register code equations in a locale with assumptions
Mon, 02 Dec 2013 20:31:54 +0100 blanchet generalized datatype code generation code so that it works with old-style and new-style (co)datatypes (as long as they are not local)
Tue, 19 Nov 2013 15:43:08 +0100 blanchet use type suffixes instead of prefixes for 'case', '(un)fold', '(co)rec'
Tue, 19 Nov 2013 14:33:20 +0100 blanchet case_if -> case_eq_if + docs
Thu, 14 Nov 2013 20:55:09 +0100 blanchet fixed type variable confusion in 'datatype_new_compat'
Wed, 13 Nov 2013 12:32:26 +0100 blanchet shortened generated property name
Tue, 12 Nov 2013 13:47:24 +0100 blanchet added convenience function
Tue, 12 Nov 2013 13:47:24 +0100 blanchet register old-style datatypes as 'Ctr_Sugar'
Tue, 12 Nov 2013 13:47:24 +0100 blanchet export useful ML function
Tue, 12 Nov 2013 13:47:24 +0100 blanchet tuned headers
Tue, 12 Nov 2013 13:47:24 +0100 blanchet moved 'Ctr_Sugar' files out of BNF, so that it can become a general-purpose abstraction
less more (0) tip