On Sat, 15 Mar 2014, Lawrence Paulson wrote:
Now, will smt2 calls be suitable for the Library and AFP?
As far as I can tell the license did not change: Z3 is non-free in the
sense of educational / non-commercial use only. This means libraries that
critically depend on Z3 would de-facto become non-free as well.
See also http://z3.codeplex.com/license
That URL is actually shown in the mini dialog that I had put there for the
old smt setup, see
http://isabelle.in.tum.de/repos/isabelle/rev/519625ec22a0
Since the message is marked-up with Url.print, the output is active in
Isabelle/jEdit: it will be given to "open" (or the equivalent of it
depending on the platform), so that the normal browser of the user can
display it. (That is just for the fun of semantic markup in Isabelle
input and output. Similar tricks work for @{file} in document soruces and
@{path} in Isabelle/ML, both for plain files and directories, e.g. in
Isabelle/3250d70c8d0b.)
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
