1.1 --- a/src/HOL/SMT.thy	Tue Mar 27 16:59:13 2012 +0300
     1.2 +++ b/src/HOL/SMT.thy	Tue Mar 27 16:59:13 2012 +0300
     1.3 @@ -272,16 +272,16 @@
     1.4  declare [[ smt_certificates = "" ]]
     1.5  
     1.6  text {*
     1.7 -The option @{text smt_fixed} controls whether only stored
     1.8 -certificates are should be used or invocation of an SMT solver is
     1.9 -allowed.  When set to @{text true}, no SMT solver will ever be
    1.10 +The option @{text smt_read_only_certificates} controls whether only
    1.11 +stored certificates are should be used or invocation of an SMT solver
    1.12 +is allowed.  When set to @{text true}, no SMT solver will ever be
    1.13  invoked and only the existing certificates found in the configured
    1.14  cache are used;  when set to @{text false} and there is no cached
    1.15  certificate for some proposition, then the configured SMT solver is
    1.16  invoked.
    1.17  *}
    1.18  
    1.19 -declare [[ smt_fixed = false ]]
    1.20 +declare [[ smt_read_only_certificates = false ]]
    1.21  
    1.22  
    1.23