src/HOL/SMT.thy
changeset 58072 a86c962de77f
parent 58061 3d060f43accb
child 58360 dee1fd1cc631
     1.1 --- a/src/HOL/SMT.thy	Thu Aug 28 16:58:26 2014 +0200
     1.2 +++ b/src/HOL/SMT.thy	Thu Aug 28 16:58:26 2014 +0200
     1.3 @@ -127,7 +127,7 @@
     1.4    Scan.optional Attrib.thms [] >>
     1.5      (fn thms => fn ctxt =>
     1.6        METHOD (fn facts => HEADGOAL (SMT_Solver.smt_tac ctxt (thms @ facts))))
     1.7 -*} "apply an SMT solver to the current goal (based on SMT-LIB 2)"
     1.8 +*} "apply an SMT solver to the current goal"
     1.9  
    1.10  
    1.11  subsection {* Configuration *}