src/HOL/Library/Old_SMT.thy
changeset 61585 a9599d3d7610
parent 60500 903bb1495239
child 64078 0b22328a353c
     1.1 --- a/src/HOL/Library/Old_SMT.thy	Thu Nov 05 10:35:37 2015 +0100
     1.2 +++ b/src/HOL/Library/Old_SMT.thy	Thu Nov 05 10:39:49 2015 +0100
     1.3 @@ -51,7 +51,7 @@
     1.4  definition weight :: "int \<Rightarrow> bool \<Rightarrow> bool" where "weight _ P = P"
     1.5  
     1.6  text \<open>
     1.7 -Weights must be non-negative.  The value @{text 0} is equivalent to providing
     1.8 +Weights must be non-negative.  The value \<open>0\<close> is equivalent to providing
     1.9  no weight at all.
    1.10  
    1.11  Weights should only be used at quantifiers and only inside triggers (if the
    1.12 @@ -150,7 +150,7 @@
    1.13  
    1.14  text \<open>
    1.15  The current configuration can be printed by the command
    1.16 -@{text old_smt_status}, which shows the values of most options.
    1.17 +\<open>old_smt_status\<close>, which shows the values of most options.
    1.18  \<close>
    1.19  
    1.20  
    1.21 @@ -158,14 +158,14 @@
    1.22  subsection \<open>General configuration options\<close>
    1.23  
    1.24  text \<open>
    1.25 -The option @{text old_smt_solver} can be used to change the target SMT
    1.26 -solver.  The possible values can be obtained from the @{text old_smt_status}
    1.27 +The option \<open>old_smt_solver\<close> can be used to change the target SMT
    1.28 +solver.  The possible values can be obtained from the \<open>old_smt_status\<close>
    1.29  command.
    1.30  
    1.31  Due to licensing restrictions, Yices and Z3 are not installed/enabled
    1.32  by default.  Z3 is free for non-commercial applications and can be enabled
    1.33 -by setting the @{text OLD_Z3_NON_COMMERCIAL} environment variable to
    1.34 -@{text yes}.
    1.35 +by setting the \<open>OLD_Z3_NON_COMMERCIAL\<close> environment variable to
    1.36 +\<open>yes\<close>.
    1.37  \<close>
    1.38  
    1.39  declare [[ old_smt_solver = z3 ]]
    1.40 @@ -242,7 +242,7 @@
    1.41  subsection \<open>Certificates\<close>
    1.42  
    1.43  text \<open>
    1.44 -By setting the option @{text old_smt_certificates} to the name of a file,
    1.45 +By setting the option \<open>old_smt_certificates\<close> to the name of a file,
    1.46  all following applications of an SMT solver a cached in that file.
    1.47  Any further application of the same SMT solver (using the very same
    1.48  configuration) re-uses the cached certificate instead of invoking the
    1.49 @@ -250,7 +250,7 @@
    1.50  
    1.51  The filename should be given as an explicit path.  It is good
    1.52  practice to use the name of the current theory (with ending
    1.53 -@{text ".certs"} instead of @{text ".thy"}) as the certificates file.
    1.54 +\<open>.certs\<close> instead of \<open>.thy\<close>) as the certificates file.
    1.55  Certificate files should be used at most once in a certain theory context,
    1.56  to avoid race conditions with other concurrent accesses.
    1.57  \<close>
    1.58 @@ -258,11 +258,11 @@
    1.59  declare [[ old_smt_certificates = "" ]]
    1.60  
    1.61  text \<open>
    1.62 -The option @{text old_smt_read_only_certificates} controls whether only
    1.63 +The option \<open>old_smt_read_only_certificates\<close> controls whether only
    1.64  stored certificates are should be used or invocation of an SMT solver
    1.65 -is allowed.  When set to @{text true}, no SMT solver will ever be
    1.66 +is allowed.  When set to \<open>true\<close>, no SMT solver will ever be
    1.67  invoked and only the existing certificates found in the configured
    1.68 -cache are used;  when set to @{text false} and there is no cached
    1.69 +cache are used;  when set to \<open>false\<close> and there is no cached
    1.70  certificate for some proposition, then the configured SMT solver is
    1.71  invoked.
    1.72  \<close>
    1.73 @@ -275,7 +275,7 @@
    1.74  
    1.75  text \<open>
    1.76  The SMT method, when applied, traces important information.  To
    1.77 -make it entirely silent, set the following option to @{text false}.
    1.78 +make it entirely silent, set the following option to \<open>false\<close>.
    1.79  \<close>
    1.80  
    1.81  declare [[ old_smt_verbose = true ]]
    1.82 @@ -283,7 +283,7 @@
    1.83  text \<open>
    1.84  For tracing the generated problem file given to the SMT solver as
    1.85  well as the returned result of the solver, the option
    1.86 -@{text old_smt_trace} should be set to @{text true}.
    1.87 +\<open>old_smt_trace\<close> should be set to \<open>true\<close>.
    1.88  \<close>
    1.89  
    1.90  declare [[ old_smt_trace = false ]]
    1.91 @@ -292,7 +292,7 @@
    1.92  From the set of assumptions given to the SMT solver, those assumptions
    1.93  used in the proof are traced when the following option is set to
    1.94  @{term true}.  This only works for Z3 when it runs in non-oracle mode
    1.95 -(see options @{text old_smt_solver} and @{text old_smt_oracle} above).
    1.96 +(see options \<open>old_smt_solver\<close> and \<open>old_smt_oracle\<close> above).
    1.97  \<close>
    1.98  
    1.99  declare [[ old_smt_trace_used_facts = false ]]
   1.100 @@ -304,9 +304,9 @@
   1.101  text \<open>
   1.102  Several prof rules of Z3 are not very well documented.  There are two
   1.103  lemma groups which can turn failing Z3 proof reconstruction attempts
   1.104 -into succeeding ones: the facts in @{text z3_rule} are tried prior to
   1.105 +into succeeding ones: the facts in \<open>z3_rule\<close> are tried prior to
   1.106  any implemented reconstruction procedure for all uncertain Z3 proof
   1.107 -rules;  the facts in @{text z3_simp} are only fed to invocations of
   1.108 +rules;  the facts in \<open>z3_simp\<close> are only fed to invocations of
   1.109  the simplifier when reconstructing theory-specific proof steps.
   1.110  \<close>
   1.111