florian.haftmann at informatik.tu-muenchen.de
Wed Sep 11 18:57:56 CEST 2013
Am 11.09.2013 11:31, schrieb C. Diekmann:
> I just downloaded the compiled binary for Linux and wanted to share my
> experience. It seems there are some issues with braces. My thy files
> work fine with the release, however, in the AFP Collections entry, I
> had to make the following changes: […]
you might consider the download »the« tip of the AFP repository:
The AFP is much more inert and less technically involved than the
Isabelle system proper, so in this case it is preferable to be hooked up
to a volatile changeset rather than doing a lot of ad-hoc adjustion.
> Finally, the following imports are no longer available:
> Something was already mentioned about this (I will investigate later).
> I cannot give feedback about the generated Scala code now as the
> change to the generated code is too huge because of this.
I guess these theories have been referenced by the AFP entries. If not,
see the NEWS
> * Discontinued theories Code_Integer and Efficient_Nat by a more
> fine-grain stack of theories Code_Target_Int, Code_Binary_Nat,
> Code_Target_Nat and Code_Target_Numeral. See the tutorial on code
> generation for details. INCOMPATIBILITY.
Hope this helps,
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 261 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev