| changeset 33465 | 8c489493e65e |
| parent 33446 | 153a27370a42 |
| child 33472 | e88f67d679c4 |
--- a/src/HOL/SMT/Examples/SMT_Examples.thy Thu Nov 05 20:42:47 2009 +0100 +++ b/src/HOL/SMT/Examples/SMT_Examples.thy Fri Nov 06 09:27:20 2009 +0100 @@ -5,7 +5,7 @@ header {* Examples for the 'smt' tactic. *} theory SMT_Examples -imports "../SMT" +imports SMT begin declare [[smt_solver=z3, z3_proofs=true]]