[isabelle-dev] smt2

[Makarius]

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