[isabelle-dev] Isabelle_10-Sep-2013

[Florian Haftmann]

Hi Cornelius,

Am 11.09.2013 11:31, schrieb C. Diekmann:
> Hi,
> 
> 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:
http://sourceforge.net/p/afp/code/ci/tip/log/

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:
> "~~/src/HOL/Library/Code_Char_chr"
> "~~/src/HOL/Library/Efficient_Nat"
> "~~/src/HOL/Library/Code_Char_ord"
> 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,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130911/d7bf40f9/attachment.sig>