| Sat, 07 Dec 2013 18:06:49 +0100 |
traytel |
code equations for "local" (co)datatypes available after interpretation of locales with assumptions
|
file |
diff |
annotate
|
| Thu, 05 Dec 2013 14:35:58 +0100 |
blanchet |
proper code generation for discriminators/selectors
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Mon, 02 Dec 2013 20:31:54 +0100 |
blanchet |
added 'no_code' option
|
file |
diff |
annotate
|
| Mon, 02 Dec 2013 20:31:54 +0100 |
blanchet |
repaired inconsistency introduced in transiting to 'Local_Theory.define'
|
file |
diff |
annotate
|
| 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)
|
file |
diff |
annotate
|
| Mon, 02 Dec 2013 20:31:54 +0100 |
blanchet |
don't try to register code equations in a locale with assumptions
|
file |
diff |
annotate
|
| 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)
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 15:43:08 +0100 |
blanchet |
use type suffixes instead of prefixes for 'case', '(un)fold', '(co)rec'
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 14:33:20 +0100 |
blanchet |
case_if -> case_eq_if + docs
|
file |
diff |
annotate
|
| Thu, 14 Nov 2013 20:55:09 +0100 |
blanchet |
fixed type variable confusion in 'datatype_new_compat'
|
file |
diff |
annotate
|
| Wed, 13 Nov 2013 12:32:26 +0100 |
blanchet |
shortened generated property name
|
file |
diff |
annotate
|
| Tue, 12 Nov 2013 13:47:24 +0100 |
blanchet |
added convenience function
|
file |
diff |
annotate
|
| Tue, 12 Nov 2013 13:47:24 +0100 |
blanchet |
register old-style datatypes as 'Ctr_Sugar'
|
file |
diff |
annotate
|
| Tue, 12 Nov 2013 13:47:24 +0100 |
blanchet |
export useful ML function
|
file |
diff |
annotate
|
| Tue, 12 Nov 2013 13:47:24 +0100 |
blanchet |
tuned headers
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
| base
|