merged
authorbulwahn
Fri Jan 07 15:59:10 2011 +0100 (2011-01-07)
changeset 4146152d39af5e680
parent 41460 ea56b98aee83
parent 41459 f0db8f40d656
child 41462 5f4939d46b63
merged
     1.1 --- a/Admin/PLATFORMS	Fri Jan 07 14:46:28 2011 +0100
     1.2 +++ b/Admin/PLATFORMS	Fri Jan 07 15:59:10 2011 +0100
     1.3 @@ -61,13 +61,13 @@
     1.4  The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
     1.5  the platform, even on 64 bit hardware.  Power-tools need to indicate
     1.6  64 bit support explicitly, via the (optional) ISABELLE_PLATFORM64
     1.7 -setting.  The following bash expressions prefers the 64 bit platform,
     1.8 +setting.  The following bash expression prefers the 64 bit platform,
     1.9  if that is available:
    1.10  
    1.11    "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
    1.12  
    1.13  Note that ML and JVM may have a different idea of the platform,
    1.14 -depending the the respective binaries that are actually run.
    1.15 +depending on the respective binaries that are actually run.
    1.16  
    1.17  
    1.18  Dependable system tools
     2.1 --- a/src/HOL/SMT.thy	Fri Jan 07 14:46:28 2011 +0100
     2.2 +++ b/src/HOL/SMT.thy	Fri Jan 07 15:59:10 2011 +0100
     2.3 @@ -178,6 +178,10 @@
     2.4  The option @{text smt_solver} can be used to change the target SMT
     2.5  solver.  The possible values can be obtained from the @{text smt_status}
     2.6  command.
     2.7 +
     2.8 +Due to licensing restrictions, Yices and Z3 are not installed/enabled
     2.9 +by default.  Z3 is free for non-commercial applications and can be enabled
    2.10 +by simply setting the environment variable Z3_NON_COMMERCIAL to @{text yes}.
    2.11  *}
    2.12  
    2.13  declare [[ smt_solver = cvc3 ]]