--- a/src/HOL/SMT.thy Sun Jan 16 21:10:30 2011 +0100
+++ b/src/HOL/SMT.thy Mon Jan 17 17:45:52 2011 +0100
@@ -185,7 +185,7 @@
@{text yes}.
*}
-declare [[ smt_solver = cvc3 ]]
+declare [[ smt_solver = z3 ]]
text {*
Since SMT solvers are potentially non-terminating, there is a timeout