src/HOL/SMT.thy
changeset 47701 157e6108a342
parent 47152 446cfc760ccf
child 48892 0b2407f406e8
     1.1 --- a/src/HOL/SMT.thy	Mon Apr 23 18:42:05 2012 +0200
     1.2 +++ b/src/HOL/SMT.thy	Mon Apr 23 21:44:36 2012 +0200
     1.3 @@ -153,13 +153,17 @@
     1.4  setup {*
     1.5    SMT_Config.setup #>
     1.6    SMT_Normalize.setup #>
     1.7 -  SMT_Solver.setup #>
     1.8    SMTLIB_Interface.setup #>
     1.9    Z3_Interface.setup #>
    1.10    Z3_Proof_Reconstruction.setup #>
    1.11    SMT_Setup_Solvers.setup
    1.12  *}
    1.13  
    1.14 +method_setup smt = {*
    1.15 +  Scan.optional Attrib.thms [] >>
    1.16 +    (fn thms => fn ctxt =>
    1.17 +      METHOD (fn facts => HEADGOAL (SMT_Solver.smt_tac ctxt (thms @ facts))))
    1.18 +*} "apply an SMT solver to the current goal"
    1.19  
    1.20  
    1.21  subsection {* Configuration *}