| Wed, 12 Feb 2014 11:28:17 +0100 |
wenzelm |
maintain blob edits within history, which is important for Snapshot.convert/revert;
|
changeset |
files
|
| Wed, 12 Feb 2014 11:05:48 +0100 |
wenzelm |
more accurate eq_content;
|
changeset |
files
|
| Wed, 12 Feb 2014 10:50:49 +0100 |
wenzelm |
clarified message_positions: cover alt_id as well;
|
changeset |
files
|
| Tue, 11 Feb 2014 21:58:31 +0100 |
wenzelm |
maintain multiple command chunks and markup trees: for main chunk and loaded files;
|
changeset |
files
|
| Tue, 11 Feb 2014 17:44:29 +0100 |
wenzelm |
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
|
changeset |
files
|
| Tue, 11 Feb 2014 15:55:05 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 11 Feb 2014 15:05:13 +0100 |
wenzelm |
report (but ignore) markup within auxiliary files;
|
changeset |
files
|
| Wed, 12 Feb 2014 10:59:25 +0100 |
Andreas Lochbihler |
merged
|
changeset |
files
|
| Wed, 12 Feb 2014 09:06:04 +0100 |
Andreas Lochbihler |
make integer_of_char and char_of_integer work with NBE and code_simp
|
changeset |
files
|
| Wed, 12 Feb 2014 08:56:38 +0100 |
Andreas Lochbihler |
make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
|
changeset |
files
|
| Wed, 12 Feb 2014 10:20:31 +0100 |
blanchet |
[mq]: news
|
changeset |
files
|
| Wed, 12 Feb 2014 08:37:28 +0100 |
blanchet |
remove hidden fact about hidden constant from code generator setup
|
changeset |
files
|
| Wed, 12 Feb 2014 08:37:28 +0100 |
blanchet |
for extraction -- use the exhaust rule that's registered with 'datatype_realizer.ML'
|
changeset |
files
|
| Wed, 12 Feb 2014 08:37:28 +0100 |
blanchet |
compile
|
changeset |
files
|
| Wed, 12 Feb 2014 08:37:28 +0100 |
blanchet |
updated certificates
|
changeset |
files
|
| Wed, 12 Feb 2014 08:37:28 +0100 |
blanchet |
tuned message
|
changeset |
files
|
| Wed, 12 Feb 2014 08:37:28 +0100 |
blanchet |
tabled, v.: postpone consideration of
|
changeset |
files
|
| Wed, 12 Feb 2014 08:37:28 +0100 |
blanchet |
adapted to renaming of 'Projl' and 'Projr'
|
changeset |
files
|
| Wed, 12 Feb 2014 08:37:06 +0100 |
blanchet |
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
|
changeset |
files
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
adapted theories to 'xxx_case' to 'case_xxx'
|
changeset |
files
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed 'nat_{case,rec}' to '{case,rec}_nat'
|
changeset |
files
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
changeset |
files
|
| 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
|
| Mon, 10 Feb 2014 22:08:18 +0100 |
wenzelm |
discontinued axiomatic 'classes', 'classrel', 'arities';
|
changeset |
files
|
| Mon, 10 Feb 2014 22:07:50 +0100 |
wenzelm |
updated keywords;
|
changeset |
files
|
| Mon, 10 Feb 2014 21:03:28 +0100 |
wenzelm |
more explicit axiomatization;
|
changeset |
files
|
| Mon, 10 Feb 2014 21:00:56 +0100 |
wenzelm |
prefer vacuous definitional type classes over axiomatic ones;
|
changeset |
files
|
| Mon, 10 Feb 2014 17:23:13 +0100 |
wenzelm |
more explicit axiomatization;
|
changeset |
files
|
| Mon, 10 Feb 2014 17:20:11 +0100 |
wenzelm |
prefer vacuous definitional type classes over axiomatic ones;
|
changeset |
files
|
| Mon, 10 Feb 2014 14:33:47 +0100 |
wenzelm |
comments;
|
changeset |
files
|
| Mon, 10 Feb 2014 13:47:31 +0100 |
wenzelm |
removed rotten code;
|
changeset |
files
|
| Mon, 10 Feb 2014 13:04:08 +0100 |
wenzelm |
more elementary put_simpset: exchange the simplifier configuration outright, which is particularly relevant concerning cumulative depth, e.g. for Product_Type.split_beta in the subsequent example:
|
changeset |
files
|
| Mon, 10 Feb 2014 21:51:15 +0100 |
nipkow |
merged
|
changeset |
files
|