src/HOL/SMT.thy
changeset 41601 fda8511006f9
parent 41462 5f4939d46b63
child 41762 00060198de12
     1.1 --- a/src/HOL/SMT.thy	Sun Jan 16 21:10:30 2011 +0100
     1.2 +++ b/src/HOL/SMT.thy	Mon Jan 17 17:45:52 2011 +0100
     1.3 @@ -185,7 +185,7 @@
     1.4  @{text yes}.
     1.5  *}
     1.6  
     1.7 -declare [[ smt_solver = cvc3 ]]
     1.8 +declare [[ smt_solver = z3 ]]
     1.9  
    1.10  text {*
    1.11  Since SMT solvers are potentially non-terminating, there is a timeout