src/HOL/SMT.thy
changeset 61799 4cf66f21b764
parent 61626 c304402cc3df
child 66298 5ff9fe3fee66
     1.1 --- a/src/HOL/SMT.thy	Mon Dec 07 10:23:50 2015 +0100
     1.2 +++ b/src/HOL/SMT.thy	Mon Dec 07 10:38:04 2015 +0100
     1.3 @@ -123,8 +123,8 @@
     1.4  subsection \<open>Integer division and modulo for Z3\<close>
     1.5  
     1.6  text \<open>
     1.7 -The following Z3-inspired definitions are overspecified for the case where @{text "l = 0"}. This
     1.8 -Schönheitsfehler is corrected in the @{text div_as_z3div} and @{text mod_as_z3mod} theorems.
     1.9 +The following Z3-inspired definitions are overspecified for the case where \<open>l = 0\<close>. This
    1.10 +Schönheitsfehler is corrected in the \<open>div_as_z3div\<close> and \<open>mod_as_z3mod\<close> theorems.
    1.11  \<close>
    1.12  
    1.13  definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where
    1.14 @@ -182,15 +182,15 @@
    1.15  
    1.16  text \<open>
    1.17  The current configuration can be printed by the command
    1.18 -@{text smt_status}, which shows the values of most options.
    1.19 +\<open>smt_status\<close>, which shows the values of most options.
    1.20  \<close>
    1.21  
    1.22  
    1.23  subsection \<open>General configuration options\<close>
    1.24  
    1.25  text \<open>
    1.26 -The option @{text smt_solver} can be used to change the target SMT
    1.27 -solver. The possible values can be obtained from the @{text smt_status}
    1.28 +The option \<open>smt_solver\<close> can be used to change the target SMT
    1.29 +solver. The possible values can be obtained from the \<open>smt_status\<close>
    1.30  command.
    1.31  \<close>
    1.32  
    1.33 @@ -258,7 +258,7 @@
    1.34  subsection \<open>Certificates\<close>
    1.35  
    1.36  text \<open>
    1.37 -By setting the option @{text smt_certificates} to the name of a file,
    1.38 +By setting the option \<open>smt_certificates\<close> to the name of a file,
    1.39  all following applications of an SMT solver a cached in that file.
    1.40  Any further application of the same SMT solver (using the very same
    1.41  configuration) re-uses the cached certificate instead of invoking the
    1.42 @@ -266,7 +266,7 @@
    1.43  
    1.44  The filename should be given as an explicit path. It is good
    1.45  practice to use the name of the current theory (with ending
    1.46 -@{text ".certs"} instead of @{text ".thy"}) as the certificates file.
    1.47 +\<open>.certs\<close> instead of \<open>.thy\<close>) as the certificates file.
    1.48  Certificate files should be used at most once in a certain theory context,
    1.49  to avoid race conditions with other concurrent accesses.
    1.50  \<close>
    1.51 @@ -274,11 +274,11 @@
    1.52  declare [[smt_certificates = ""]]
    1.53  
    1.54  text \<open>
    1.55 -The option @{text smt_read_only_certificates} controls whether only
    1.56 +The option \<open>smt_read_only_certificates\<close> controls whether only
    1.57  stored certificates are should be used or invocation of an SMT solver
    1.58 -is allowed. When set to @{text true}, no SMT solver will ever be
    1.59 +is allowed. When set to \<open>true\<close>, no SMT solver will ever be
    1.60  invoked and only the existing certificates found in the configured
    1.61 -cache are used;  when set to @{text false} and there is no cached
    1.62 +cache are used;  when set to \<open>false\<close> and there is no cached
    1.63  certificate for some proposition, then the configured SMT solver is
    1.64  invoked.
    1.65  \<close>
    1.66 @@ -290,7 +290,7 @@
    1.67  
    1.68  text \<open>
    1.69  The SMT method, when applied, traces important information. To
    1.70 -make it entirely silent, set the following option to @{text false}.
    1.71 +make it entirely silent, set the following option to \<open>false\<close>.
    1.72  \<close>
    1.73  
    1.74  declare [[smt_verbose = true]]
    1.75 @@ -298,7 +298,7 @@
    1.76  text \<open>
    1.77  For tracing the generated problem file given to the SMT solver as
    1.78  well as the returned result of the solver, the option
    1.79 -@{text smt_trace} should be set to @{text true}.
    1.80 +\<open>smt_trace\<close> should be set to \<open>true\<close>.
    1.81  \<close>
    1.82  
    1.83  declare [[smt_trace = false]]
    1.84 @@ -309,9 +309,9 @@
    1.85  text \<open>
    1.86  Several prof rules of Z3 are not very well documented. There are two
    1.87  lemma groups which can turn failing Z3 proof reconstruction attempts
    1.88 -into succeeding ones: the facts in @{text z3_rule} are tried prior to
    1.89 +into succeeding ones: the facts in \<open>z3_rule\<close> are tried prior to
    1.90  any implemented reconstruction procedure for all uncertain Z3 proof
    1.91 -rules;  the facts in @{text z3_simp} are only fed to invocations of
    1.92 +rules;  the facts in \<open>z3_simp\<close> are only fed to invocations of
    1.93  the simplifier when reconstructing theory-specific proof steps.
    1.94  \<close>
    1.95