1.1 --- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Tue Mar 27 16:59:13 2012 +0300
     1.2 +++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Tue Mar 27 16:59:13 2012 +0300
     1.3 @@ -82,9 +82,9 @@
     1.4  
     1.5  boogie_open "Boogie_Dijkstra.b2i"
     1.6  
     1.7 -declare [[smt_certificates="Boogie_Dijkstra.certs"]]
     1.8 -declare [[smt_fixed=true]]
     1.9 -declare [[smt_oracle=false]]
    1.10 +declare [[smt_certificates = "Boogie_Dijkstra.certs"]]
    1.11 +declare [[smt_read_only_certificates = true]]
    1.12 +declare [[smt_oracle = false]]
    1.13  
    1.14  boogie_vc Dijkstra
    1.15    by boogie

     2.1 --- a/src/HOL/Boogie/Examples/Boogie_Max.thy	Tue Mar 27 16:59:13 2012 +0300
     2.2 +++ b/src/HOL/Boogie/Examples/Boogie_Max.thy	Tue Mar 27 16:59:13 2012 +0300
     2.3 @@ -39,9 +39,9 @@
     2.4  
     2.5  boogie_open "Boogie_Max.b2i"
     2.6  
     2.7 -declare [[smt_certificates="Boogie_Max.certs"]]
     2.8 -declare [[smt_fixed=true]]
     2.9 -declare [[smt_oracle=false]]
    2.10 +declare [[smt_certificates = "Boogie_Max.certs"]]
    2.11 +declare [[smt_read_only_certificates = true]]
    2.12 +declare [[smt_oracle = false]]
    2.13  
    2.14  boogie_vc max
    2.15    by boogie

     3.1 --- a/src/HOL/Boogie/Examples/VCC_Max.thy	Tue Mar 27 16:59:13 2012 +0300
     3.2 +++ b/src/HOL/Boogie/Examples/VCC_Max.thy	Tue Mar 27 16:59:13 2012 +0300
     3.3 @@ -47,9 +47,9 @@
     3.4  
     3.5  boogie_open (quiet) "VCC_Max.b2i"
     3.6  
     3.7 -declare [[smt_certificates="VCC_Max.certs"]]
     3.8 -declare [[smt_fixed=true]]
     3.9 -declare [[smt_oracle=false]]
    3.10 +declare [[smt_certificates = "VCC_Max.certs"]]
    3.11 +declare [[smt_read_only_certificates = true]]
    3.12 +declare [[smt_oracle = false]]
    3.13  
    3.14  boogie_status
    3.15  

     4.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 27 16:59:13 2012 +0300
     4.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 27 16:59:13 2012 +0300
     4.3 @@ -8,9 +8,9 @@
     4.4    "~~/src/HOL/Library/Indicator_Function"
     4.5  begin
     4.6  
     4.7 -declare [[smt_certificates="Integration.certs"]]
     4.8 -declare [[smt_fixed=true]]
     4.9 -declare [[smt_oracle=false]]
    4.10 +declare [[smt_certificates = "Integration.certs"]]
    4.11 +declare [[smt_read_only_certificates = true]]
    4.12 +declare [[smt_oracle = false]]
    4.13  
    4.14  (*declare not_less[simp] not_le[simp]*)
    4.15  
    4.16 @@ -5583,7 +5583,7 @@
    4.17              using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto
    4.18          qed qed(insert n,auto) qed qed qed
    4.19  
    4.20 -declare [[smt_certificates=""]]
    4.21 -declare [[smt_fixed=false]]
    4.22 +declare [[smt_certificates = ""]]
    4.23 +declare [[smt_read_only_certificates = false]]
    4.24  
    4.25  end

     5.1 --- a/src/HOL/SMT.thy	Tue Mar 27 16:59:13 2012 +0300
     5.2 +++ b/src/HOL/SMT.thy	Tue Mar 27 16:59:13 2012 +0300
     5.3 @@ -272,16 +272,16 @@
     5.4  declare [[ smt_certificates = "" ]]
     5.5  
     5.6  text {*
     5.7 -The option @{text smt_fixed} controls whether only stored
     5.8 -certificates are should be used or invocation of an SMT solver is
     5.9 -allowed.  When set to @{text true}, no SMT solver will ever be
    5.10 +The option @{text smt_read_only_certificates} controls whether only
    5.11 +stored certificates are should be used or invocation of an SMT solver
    5.12 +is allowed.  When set to @{text true}, no SMT solver will ever be
    5.13  invoked and only the existing certificates found in the configured
    5.14  cache are used;  when set to @{text false} and there is no cached
    5.15  certificate for some proposition, then the configured SMT solver is
    5.16  invoked.
    5.17  *}
    5.18  
    5.19 -declare [[ smt_fixed = false ]]
    5.20 +declare [[ smt_read_only_certificates = false ]]
    5.21  
    5.22  
    5.23  

     6.1 --- a/src/HOL/SMT_Examples/SMT_Examples.thy	Tue Mar 27 16:59:13 2012 +0300
     6.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Tue Mar 27 16:59:13 2012 +0300
     6.3 @@ -8,9 +8,9 @@
     6.4  imports Complex_Main
     6.5  begin
     6.6  
     6.7 -declare [[smt_oracle=false]]
     6.8 -declare [[smt_certificates="SMT_Examples.certs"]]
     6.9 -declare [[smt_fixed=true]]
    6.10 +declare [[smt_oracle = false]]
    6.11 +declare [[smt_certificates = "SMT_Examples.certs"]]
    6.12 +declare [[smt_read_only_certificates = true]]
    6.13  
    6.14  
    6.15  

     7.1 --- a/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Mar 27 16:59:13 2012 +0300
     7.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Mar 27 16:59:13 2012 +0300
     7.3 @@ -8,9 +8,9 @@
     7.4  imports Complex_Main
     7.5  begin
     7.6  
     7.7 -declare [[smt_oracle=false]]
     7.8 -declare [[smt_certificates="SMT_Tests.certs"]]
     7.9 -declare [[smt_fixed=true]]
    7.10 +declare [[smt_oracle = false]]
    7.11 +declare [[smt_certificates = "SMT_Tests.certs"]]
    7.12 +declare [[smt_read_only_certificates = true]]
    7.13  
    7.14  
    7.15  

     8.1 --- a/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Tue Mar 27 16:59:13 2012 +0300
     8.2 +++ b/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Tue Mar 27 16:59:13 2012 +0300
     8.3 @@ -8,9 +8,9 @@
     8.4  imports Word
     8.5  begin
     8.6  
     8.7 -declare [[smt_oracle=true]]
     8.8 -declare [[smt_certificates="SMT_Word_Examples.certs"]]
     8.9 -declare [[smt_fixed=true]]
    8.10 +declare [[smt_oracle = true]]
    8.11 +declare [[smt_certificates = "SMT_Word_Examples.certs"]]
    8.12 +declare [[smt_read_only_certificates = true]]
    8.13  
    8.14  
    8.15  

     9.1 --- a/src/HOL/Tools/SMT/smt_config.ML	Tue Mar 27 16:59:13 2012 +0300
     9.2 +++ b/src/HOL/Tools/SMT/smt_config.ML	Tue Mar 27 16:59:13 2012 +0300
     9.3 @@ -26,7 +26,7 @@
     9.4    val datatypes: bool Config.T
     9.5    val timeout: real Config.T
     9.6    val random_seed: int Config.T
     9.7 -  val fixed: bool Config.T
     9.8 +  val read_only_certificates: bool Config.T
     9.9    val verbose: bool Config.T
    9.10    val trace: bool Config.T
    9.11    val trace_used_facts: bool Config.T
    9.12 @@ -153,7 +153,7 @@
    9.13  val datatypes = Attrib.setup_config_bool @{binding smt_datatypes} (K false)
    9.14  val timeout = Attrib.setup_config_real @{binding smt_timeout} (K 30.0)
    9.15  val random_seed = Attrib.setup_config_int @{binding smt_random_seed} (K 1)
    9.16 -val fixed = Attrib.setup_config_bool @{binding smt_fixed} (K false)
    9.17 +val read_only_certificates = Attrib.setup_config_bool @{binding smt_read_only_certificates} (K false)
    9.18  val verbose = Attrib.setup_config_bool @{binding smt_verbose} (K true)
    9.19  val trace = Attrib.setup_config_bool @{binding smt_trace} (K false)
    9.20  val trace_used_facts = Attrib.setup_config_bool @{binding smt_trace_used_facts} (K false)
    9.21 @@ -243,7 +243,7 @@
    9.22          string_of_bool (not (Config.get ctxt oracle))),
    9.23        Pretty.str ("Certificates cache: " ^ certs_filename),
    9.24        Pretty.str ("Fixed certificates: " ^
    9.25 -        string_of_bool (Config.get ctxt fixed))])
    9.26 +        string_of_bool (Config.get ctxt read_only_certificates))])
    9.27    end
    9.28  
    9.29  val _ =

    10.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Tue Mar 27 16:59:13 2012 +0300
    10.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Tue Mar 27 16:59:13 2012 +0300
    10.3 @@ -79,8 +79,8 @@
    10.4    | SOME certs =>
    10.5        (case Cache_IO.lookup certs input of
    10.6          (NONE, key) =>
    10.7 -          if Config.get ctxt SMT_Config.fixed then
    10.8 -            error ("Bad certificates cache: missing certificate")
    10.9 +          if Config.get ctxt SMT_Config.read_only_certificates then
   10.10 +            error ("Bad certificate cache: missing certificate")
   10.11            else
   10.12              Cache_IO.run_and_cache certs key mk_cmd input
   10.13        | (SOME output, _) =>