# HG changeset patch
# User bulwahn
# Date 1294412350 -3600
# Node ID 52d39af5e6809fa9ad282917e87fcfa83b5716a4
# Parent  ea56b98aee83f14acb8f427bd159d96d0de54aec# Parent  f0db8f40d6568501d76952d67d8c1fd77d6d40d7
merged

diff -r ea56b98aee83 -r 52d39af5e680 Admin/PLATFORMS
--- a/Admin/PLATFORMS	Fri Jan 07 14:46:28 2011 +0100
+++ b/Admin/PLATFORMS	Fri Jan 07 15:59:10 2011 +0100
@@ -61,13 +61,13 @@
 The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
 the platform, even on 64 bit hardware.  Power-tools need to indicate
 64 bit support explicitly, via the (optional) ISABELLE_PLATFORM64
-setting.  The following bash expressions prefers the 64 bit platform,
+setting.  The following bash expression prefers the 64 bit platform,
 if that is available:
 
   "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
 
 Note that ML and JVM may have a different idea of the platform,
-depending the the respective binaries that are actually run.
+depending on the respective binaries that are actually run.
 
 
 Dependable system tools
diff -r ea56b98aee83 -r 52d39af5e680 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Fri Jan 07 14:46:28 2011 +0100
+++ b/src/HOL/SMT.thy	Fri Jan 07 15:59:10 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 ]]