src/HOL/SMT.thy
changeset 41462 5f4939d46b63
parent 41459 f0db8f40d656
child 41601 fda8511006f9
     1.1 --- a/src/HOL/SMT.thy	Fri Jan 07 15:59:10 2011 +0100
     1.2 +++ b/src/HOL/SMT.thy	Fri Jan 07 17:58:51 2011 +0100
     1.3 @@ -181,7 +181,8 @@
     1.4  
     1.5  Due to licensing restrictions, Yices and Z3 are not installed/enabled
     1.6  by default.  Z3 is free for non-commercial applications and can be enabled
     1.7 -by simply setting the environment variable Z3_NON_COMMERCIAL to @{text yes}.
     1.8 +by simply setting the environment variable @{text Z3_NON_COMMERCIAL} to
     1.9 +@{text yes}.
    1.10  *}
    1.11  
    1.12  declare [[ smt_solver = cvc3 ]]