| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
adapted theories to '{case,rec}_{list,option}' names
|
changeset |
files
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
avoid old 'prod.simps' -- better be more specific
|
changeset |
files
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
repaired hard-coded constant names
|
changeset |
files
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
killed 'rep_compat' option
|
changeset |
files
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
made 'ctr_sugar' more friendly to the 'datatype_realizer'
|
changeset |
files
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
use names like 'rec_mytype' and 'case_mytype' in old datatype package as well, to avoid a mixture
|
changeset |
files
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
use right local theory -- shows up when 'no_discs_sels' is set
|
changeset |
files
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
compatibility names
|
changeset |
files
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
use new selector support to define 'the', 'hd', 'tl'
|
changeset |
files
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well)
|
changeset |
files
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
avoid duplicate 'case' definitions by first looking up 'Ctr_Sugar'
|
changeset |
files
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
tuned code
|
changeset |
files
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
more 'ctr_sugar' modernization
|
changeset |
files
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
ported predicate compiler to 'ctr_sugar'
|
changeset |
files
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
updated docs
|
changeset |
files
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
generate 'fundec_cong' attribute for new-style (co)datatypes
|
changeset |
files
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
got rid of dynamic scoping the easy way
|
changeset |
files
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
removed trivial 'rec' examples for nonrecursive types (I could also have added the 'old.' prefix in front of the constant names)
|
changeset |
files
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
more liberal merging of BNFs and constructor sugar
|
changeset |
files
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
|
changeset |
files
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
have the same no-update semantics for 'case' as for 'Ctr_Sugar' and BNF data (this might not be the final word on the matter, but using a consistent policy seems like a good idea)
|
changeset |
files
|
| Tue, 11 Feb 2014 12:08:44 +0100 |
wenzelm |
Mac OS X Lion (macbroy6) is baseline for portable executables;
|
changeset |
files
|
| Tue, 11 Feb 2014 11:30:33 +0100 |
Lars Hupel |
"no_memory" option for the simplifier trace to bypass memoization
|
changeset |
files
|
| Tue, 11 Feb 2014 09:29:46 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Mon, 10 Feb 2014 23:24:44 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 10 Feb 2014 22:39:04 +0100 |
wenzelm |
seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
|
changeset |
files
|
| Mon, 10 Feb 2014 22:22:06 +0100 |
wenzelm |
make triple-sure that the future scheduler is properly shutdown (see also 702278df3b57);
|
changeset |
files
|