| Thu, 05 Dec 2013 14:11:45 +0100 |
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 |
added 'no_code' option
|
file | diff | annotate |
| Mon, 02 Dec 2013 20:31:54 +0100 |
repaired inconsistency introduced in transiting to 'Local_Theory.define'
|
file | diff | annotate |
| Mon, 02 Dec 2013 20:31:54 +0100 |
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 |
don't try to register code equations in a locale with assumptions
|
file | diff | annotate |
| Mon, 02 Dec 2013 20:31:54 +0100 |
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 |
use type suffixes instead of prefixes for 'case', '(un)fold', '(co)rec'
|
file | diff | annotate |
| Tue, 19 Nov 2013 14:33:20 +0100 |
case_if -> case_eq_if + docs
|
file | diff | annotate |
| Thu, 14 Nov 2013 20:55:09 +0100 |
fixed type variable confusion in 'datatype_new_compat'
|
file | diff | annotate |
| Wed, 13 Nov 2013 12:32:26 +0100 |
shortened generated property name
|
file | diff | annotate |
| Tue, 12 Nov 2013 13:47:24 +0100 |
added convenience function
|
file | diff | annotate |
| Tue, 12 Nov 2013 13:47:24 +0100 |
register old-style datatypes as 'Ctr_Sugar'
|
file | diff | annotate |
| Tue, 12 Nov 2013 13:47:24 +0100 |
export useful ML function
|
file | diff | annotate |
| Tue, 12 Nov 2013 13:47:24 +0100 |
tuned headers
|
file | diff | annotate |
| Tue, 12 Nov 2013 13:47:24 +0100 |
moved 'Ctr_Sugar' files out of BNF, so that it can become a general-purpose abstraction
|
file | diff | annotate | base |