changeset 41462 | 5f4939d46b63 |
parent 41459 | f0db8f40d656 |
child 41601 | fda8511006f9 |
--- 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 ]]