| 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
|