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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
