diff -r 7f58a9a843c2 -r a462d5207aa6 src/HOL/SMT_Examples/SMT_Tests.thy
--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Oct 26 11:45:12 2010 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Oct 26 11:46:19 2010 +0200
@@ -8,7 +8,7 @@
 imports Complex_Main
 begin
 
-declare [[smt_solver=z3, z3_proofs=true]]
+declare [[smt_solver=z3, smt_oracle=false]]
 declare [[smt_certificates="~~/src/HOL/SMT_Examples/SMT_Tests.certs"]]
 declare [[smt_fixed=true]]
 
@@ -145,7 +145,7 @@
   "\<exists>x. P x \<longrightarrow> P a \<and> P b"
   "\<exists>x. (\<exists>y. P y) \<longrightarrow> P x" 
   "(\<exists>x. Q \<longrightarrow> P x) \<longleftrightarrow> (Q \<longrightarrow> (\<exists>x. P x))"
-  using [[z3_proofs=false, z3_options="AUTO_CONFIG=false SATURATE=true"]]
+  using [[smt_oracle=true, z3_options="AUTO_CONFIG=false SATURATE=true"]]
   by smt+
 
 lemma
@@ -165,7 +165,7 @@
   "(\<exists>x. \<forall>y. P x \<longleftrightarrow> P y) \<longrightarrow> ((\<exists>x. P x) \<longleftrightarrow> (\<forall>y. P y))"
   "\<exists>z. P z \<longrightarrow> (\<forall>x. P x)"
   "(\<exists>y. \<forall>x. R x y) \<longrightarrow> (\<forall>x. \<exists>y. R x y)"
-  using [[z3_proofs=false]]
+  using [[smt_oracle=true]]
   by smt+
 
 lemma
@@ -622,6 +622,7 @@
   "p1 = (x, y) \<and> p2 = (y, x) \<longrightarrow> fst p1 = snd p2"
   "(fst (x, y) = snd (x, y)) = (x = y)"
   "(fst p = snd p) = (p = (snd p, fst p))"
+  using [[smt_trace=true]]
   by smt+