src/HOL/SMT.thy

--- a/src/HOL/SMT.thy	Thu Aug 28 16:58:26 2014 +0200
+++ b/src/HOL/SMT.thy	Thu Aug 28 16:58:26 2014 +0200
@@ -127,7 +127,7 @@
   Scan.optional Attrib.thms [] >>
     (fn thms => fn ctxt =>
       METHOD (fn facts => HEADGOAL (SMT_Solver.smt_tac ctxt (thms @ facts))))
-*} "apply an SMT solver to the current goal (based on SMT-LIB 2)"
+*} "apply an SMT solver to the current goal"
 
 
 subsection {* Configuration *}