src/HOL/SMT.thy
changeset 40424 7550b2cba1cb
parent 40277 4e3a3461c1a6
child 40662 798aad2229c0
     1.1 --- a/src/HOL/SMT.thy	Mon Nov 08 11:49:28 2010 +0100
     1.2 +++ b/src/HOL/SMT.thy	Mon Nov 08 12:13:44 2010 +0100
     1.3 @@ -8,7 +8,9 @@
     1.4  imports List
     1.5  uses
     1.6    "Tools/Datatype/datatype_selectors.ML"
     1.7 -  ("Tools/SMT/smt_monomorph.ML")
     1.8 +  "Tools/SMT/smt_failure.ML"
     1.9 +  "Tools/SMT/smt_config.ML"
    1.10 +  "Tools/SMT/smt_monomorph.ML"
    1.11    ("Tools/SMT/smt_builtin.ML")
    1.12    ("Tools/SMT/smt_normalize.ML")
    1.13    ("Tools/SMT/smt_translate.ML")
    1.14 @@ -126,7 +128,6 @@
    1.15  
    1.16  subsection {* Setup *}
    1.17  
    1.18 -use "Tools/SMT/smt_monomorph.ML"
    1.19  use "Tools/SMT/smt_builtin.ML"
    1.20  use "Tools/SMT/smt_normalize.ML"
    1.21  use "Tools/SMT/smt_translate.ML"
    1.22 @@ -141,6 +142,7 @@
    1.23  use "Tools/SMT/smt_setup_solvers.ML"
    1.24  
    1.25  setup {*
    1.26 +  SMT_Config.setup #>
    1.27    SMT_Solver.setup #>
    1.28    Z3_Proof_Reconstruction.setup #>
    1.29    SMT_Setup_Solvers.setup
    1.30 @@ -241,6 +243,13 @@
    1.31  subsection {* Tracing *}
    1.32  
    1.33  text {*
    1.34 +The SMT method, when applied, traces important information.  To
    1.35 +make it entirely silent, set the following option to @{text false}.
    1.36 +*}
    1.37 +
    1.38 +declare [[ smt_verbose = true ]]
    1.39 +
    1.40 +text {*
    1.41  For tracing the generated problem file given to the SMT solver as
    1.42  well as the returned result of the solver, the option
    1.43  @{text smt_trace} should be set to @{text true}.