# HG changeset patch
# User boehmes
# Date 1270662538 -7200
# Node ID 70deefb6c093593237715e1852174ebd811f724d
# Parent  0d9affa4e73c8251cec42391d0fb3caa6c9c32ba
renamed "smt_record" to "smt_fixed" (somewhat more expressive) and inverted its semantics

diff -r 0d9affa4e73c -r 70deefb6c093 src/HOL/Boogie/Examples/Boogie_Dijkstra.thy
--- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Wed Apr 07 17:24:44 2010 +0200
+++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Wed Apr 07 19:48:58 2010 +0200
@@ -82,7 +82,7 @@
 boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Dijkstra"
 
 declare [[smt_certificates="~~/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs"]]
-declare [[smt_record=false]]
+declare [[smt_fixed=true]]
 
 boogie_vc Dijkstra
   using [[z3_proofs=true]]
diff -r 0d9affa4e73c -r 70deefb6c093 src/HOL/Boogie/Examples/Boogie_Max.thy
--- a/src/HOL/Boogie/Examples/Boogie_Max.thy	Wed Apr 07 17:24:44 2010 +0200
+++ b/src/HOL/Boogie/Examples/Boogie_Max.thy	Wed Apr 07 19:48:58 2010 +0200
@@ -39,7 +39,7 @@
 boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Max"
 
 declare [[smt_certificates="~~/src/HOL/Boogie/Examples/Boogie_Max.certs"]]
-declare [[smt_record=false]]
+declare [[smt_fixed=true]]
 
 boogie_vc max
   using [[z3_proofs=true]]
diff -r 0d9affa4e73c -r 70deefb6c093 src/HOL/Boogie/Examples/VCC_Max.thy
--- a/src/HOL/Boogie/Examples/VCC_Max.thy	Wed Apr 07 17:24:44 2010 +0200
+++ b/src/HOL/Boogie/Examples/VCC_Max.thy	Wed Apr 07 19:48:58 2010 +0200
@@ -47,7 +47,7 @@
 boogie_open (quiet) "~~/src/HOL/Boogie/Examples/VCC_Max"
 
 declare [[smt_certificates="~~/src/HOL/Boogie/Examples/VCC_Max.certs"]]
-declare [[smt_record=false]]
+declare [[smt_fixed=true]]
 
 boogie_status
 
diff -r 0d9affa4e73c -r 70deefb6c093 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Wed Apr 07 17:24:44 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Apr 07 19:48:58 2010 +0200
@@ -8,7 +8,7 @@
 begin
 
 declare [[smt_certificates="~~/src/HOL/Multivariate_Analysis/Integration.cert"]]
-declare [[smt_record=false]]
+declare [[smt_fixed=true]]
 declare [[z3_proofs=true]]
 
 lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
diff -r 0d9affa4e73c -r 70deefb6c093 src/HOL/SMT/Examples/SMT_Examples.thy
--- a/src/HOL/SMT/Examples/SMT_Examples.thy	Wed Apr 07 17:24:44 2010 +0200
+++ b/src/HOL/SMT/Examples/SMT_Examples.thy	Wed Apr 07 19:48:58 2010 +0200
@@ -17,7 +17,7 @@
 the following option is set to "false":
 *}
 
-declare [[smt_record=false]]
+declare [[smt_fixed=true]]
 
 
 
diff -r 0d9affa4e73c -r 70deefb6c093 src/HOL/SMT/SMT.thy
--- a/src/HOL/SMT/SMT.thy	Wed Apr 07 17:24:44 2010 +0200
+++ b/src/HOL/SMT/SMT.thy	Wed Apr 07 19:48:58 2010 +0200
@@ -62,11 +62,11 @@
 
 declare [[ smt_certificates = "" ]]
 
-text {* Enables or disables the addition of new certificates to
-the current certificates file (when disabled, only existing
-certificates are used and no SMT solver is invoked): *}
+text {* Allows or disallows the addition of new certificates to
+the current certificates file (when set to @{text false}, only
+existing certificates are used and no SMT solver is invoked): *}
 
-declare [[ smt_record = true ]]
+declare [[ smt_fixed = false ]]
 
 
 subsection {* Special configuration options *}
diff -r 0d9affa4e73c -r 70deefb6c093 src/HOL/SMT/Tools/smt_solver.ML
--- a/src/HOL/SMT/Tools/smt_solver.ML	Wed Apr 07 17:24:44 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_solver.ML	Wed Apr 07 19:48:58 2010 +0200
@@ -30,7 +30,7 @@
   val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
 
   (*certificates*)
-  val record: bool Config.T
+  val fixed_certificates: bool Config.T
   val select_certificates: string -> Context.generic -> Context.generic
 
   (*solvers*)
@@ -93,7 +93,8 @@
 
 (* SMT certificates *)
 
-val (record, setup_record) = Attrib.config_bool "smt_record" (K true)
+val (fixed_certificates, setup_fixed_certificates) =
+  Attrib.config_bool "smt_fixed" (K false)
 
 structure Certificates = Generic_Data
 (
@@ -157,7 +158,7 @@
   in
     if is_none certs 
     then Cache_IO.run' (make_cmd (choose cmd) args) problem_path
-    else if Config.get ctxt record
+    else if Config.get ctxt fixed_certificates
     then Cache_IO.cached' (the certs) (make_cmd (choose cmd) args) problem_path
     else
      (tracing ("Using cached certificate from " ^
@@ -285,7 +286,7 @@
     "SMT solver configuration" #>
   setup_timeout #>
   setup_trace #>
-  setup_record #>
+  setup_fixed_certificates #>
   Attrib.setup (Binding.name "smt_certificates")
     (Scan.lift (OuterParse.$$$ "=" |-- Args.name) >>
       (Thm.declaration_attribute o K o select_certificates))