# HG changeset patch
# User boehmes
# Date 1294411153 -3600
# Node ID f0db8f40d6568501d76952d67d8c1fd77d6d40d7
# Parent  5eca258324ca0cf5e35f8e0e3549d12a3476259f
added hints about licensing restrictions and how to enable Z3

diff -r 5eca258324ca -r f0db8f40d656 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Fri Jan 07 15:37:53 2011 +0100
+++ b/src/HOL/SMT.thy	Fri Jan 07 15:39:13 2011 +0100
@@ -178,6 +178,10 @@
 The option @{text smt_solver} can be used to change the target SMT
 solver.  The possible values can be obtained from the @{text smt_status}
 command.
+
+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}.
 *}
 
 declare [[ smt_solver = cvc3 ]]