Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
explicit link to Z3 license;
authorwenzelm
Fri, 28 Feb 2014 17:31:19 +0100
changeset 55806 519625ec22a0
parent 55805 f4e9517657b1
child 55809 d27e7872dd10
explicit link to Z3 license;
src/HOL/Tools/SMT/smt_setup_solvers.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Fri Feb 28 15:20:18 2014 +0100
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Fri Feb 28 17:31:19 2014 +0100
@@ -117,10 +117,13 @@
       error (Pretty.string_of (Pretty.para
         "The SMT solver Z3 may only be used for non-commercial applications."))
   | Z3_Non_Commercial_Unknown =>
-      error (Pretty.string_of (Pretty.para
-        ("The SMT solver Z3 is not activated. To activate it, set the Isabelle \
-         \system option \"z3_non_commercial\" to \"yes\" (e.g. via \
-         \the Isabelle/jEdit menu Plugin Options / Isabelle / General)."))))
+      error
+        (Pretty.string_of
+          (Pretty.para
+            ("The SMT solver Z3 is not activated. To activate it, set the Isabelle \
+             \system option \"z3_non_commercial\" to \"yes\" (e.g. via \
+             \the Isabelle/jEdit menu Plugin Options / Isabelle / General).")) ^
+        "\n\nSee also " ^ Url.print (Url.explode "http://z3.codeplex.com/license")))
 
 end
isabelle