# HG changeset patch # User wenzelm # Date 1358028441 -3600 # Node ID c091e46ec3c518fa0c28c2b3148cc869c3f5fefb # Parent 3f9a24e7349e86922116473cb06d5668266b88b1 tuned message; diff -r 3f9a24e7349e -r c091e46ec3c5 src/HOL/Tools/SMT/smt_setup_solvers.ML --- a/src/HOL/Tools/SMT/smt_setup_solvers.ML Sat Jan 12 22:14:29 2013 +0100 +++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML Sat Jan 12 23:07:21 2013 +0100 @@ -130,7 +130,8 @@ "applications.") | Z3_Non_Commercial_Unknown => error ("The SMT solver Z3 is not activated. To activate it, set\n" ^ - "the environment variable " ^ quote flagN ^ " to " ^ quote "yes" ^ "." ^ + "the environment variable " ^ quote flagN ^ " to " ^ quote "yes" ^ ",\n" ^ + "and restart the Isabelle system." ^ (if getenv "Z3_COMPONENT" = "" then "" else "\nSee also " ^ Path.print (Path.expand (Path.explode "$Z3_COMPONENT/etc/settings")))))