# HG changeset patch
# User boehmes
# Date 1294419531 -3600
# Node ID 5f4939d46b635ba11ce6051652ddf70e9a6c8a6e
# Parent  52d39af5e6809fa9ad282917e87fcfa83b5716a4
tuned text

diff -r 52d39af5e680 -r 5f4939d46b63 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Fri Jan 07 15:59:10 2011 +0100
+++ b/src/HOL/SMT.thy	Fri Jan 07 17:58:51 2011 +0100
@@ -181,7 +181,8 @@
 
 Due to licensing restrictions, Yices and Z3 are not installed/enabled
 by default.  Z3 is free for non-commercial applications and can be enabled
-by simply setting the environment variable Z3_NON_COMMERCIAL to @{text yes}.
+by simply setting the environment variable @{text Z3_NON_COMMERCIAL} to
+@{text yes}.
 *}
 
 declare [[ smt_solver = cvc3 ]]