Andreas Lochbihler [Wed, 12 Feb 2014 08:56:38 +0100] rev 55426
make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
blanchet [Wed, 12 Feb 2014 10:20:31 +0100] rev 55425
[mq]: news
blanchet [Wed, 12 Feb 2014 08:37:28 +0100] rev 55424
remove hidden fact about hidden constant from code generator setup
blanchet [Wed, 12 Feb 2014 08:37:28 +0100] rev 55423
for extraction -- use the exhaust rule that's registered with 'datatype_realizer.ML'
blanchet [Wed, 12 Feb 2014 08:37:28 +0100] rev 55422
compile
blanchet [Wed, 12 Feb 2014 08:37:28 +0100] rev 55421
updated certificates
blanchet [Wed, 12 Feb 2014 08:37:28 +0100] rev 55420
tuned message
blanchet [Wed, 12 Feb 2014 08:37:28 +0100] rev 55419
tabled, v.: postpone consideration of
blanchet [Wed, 12 Feb 2014 08:37:28 +0100] rev 55418
adapted to renaming of 'Projl' and 'Projr'
blanchet [Wed, 12 Feb 2014 08:37:06 +0100] rev 55417
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
* * *
more transition of 'xxx_rec' to 'rec_xxx' and same for case
* * *
compile
* * *
'rename_tac's to avoid referring to generated names
* * *
more robust scripts with 'rename_tac'
* * *
'where' -> 'of'
* * *
'where' -> 'of'
* * *
renamed 'xxx_rec' to 'rec_xxx'