--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML Fri Feb 28 18:11:02 2014 +0100
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML Fri Feb 28 18:11:11 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