src/HOL/SMT_Examples/SMT_Tests.thy

   "(\<exists>x. P x) \<and> R \<longleftrightarrow> (\<exists>x. P x \<and> R)"
   "(\<exists>x y z. S x z) \<longleftrightarrow> (\<exists>x z. S x z)"
   "\<not>((\<exists>x. \<not>P x) \<and> ((\<exists>x. P x) \<or> (\<exists>x. P x \<and> Q x)) \<and> \<not>(\<exists>x. P x))"
   by smt+
 
-lemma  (* only without proofs: *)
+lemma
   "\<exists>x y. x = y"
   "\<exists>x. P x \<longrightarrow> (\<exists>y. P x \<and> P y)"
   "(\<exists>x. P x) \<or> R \<longleftrightarrow> (\<exists>x. P x \<or> R)"
   "\<exists>x. P x \<longrightarrow> P a \<and> P b"
-  "\<exists>x. (\<exists>y. P y) \<longrightarrow> P x" 
+  "\<exists>x. (\<exists>y. P y) \<longrightarrow> P x"
   "(\<exists>x. Q \<longrightarrow> P x) \<longleftrightarrow> (Q \<longrightarrow> (\<exists>x. P x))"
-  using [[smt_oracle=true, z3_options="AUTO_CONFIG=false SATURATE=true"]]
-  by smt+
+by smt+
 
 lemma
   "(\<not>(\<exists>x. P x)) \<longleftrightarrow> (\<forall>x. \<not> P x)"
   "(\<exists>x. P x \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P x) \<longrightarrow> Q"
   "(\<forall>x y. R x y = x) \<longrightarrow> (\<exists>y. R x y) = R x c"
   "(if P x then \<not>(\<exists>y. P y) else (\<forall>y. \<not>P y)) \<longrightarrow> P x \<longrightarrow> P y"
   "(\<forall>x y. R x y = x) \<and> (\<forall>x. \<exists>y. R x y) = (\<forall>x. R x c) \<longrightarrow> (\<exists>y. R x y) = R x c"
   by smt+
 
-lemma  (* only without proofs: *)
+lemma
   "\<forall>x. \<exists>y. f x y = f x (g x)"
   "(\<not>\<not>(\<exists>x. P x)) \<longleftrightarrow> (\<not>(\<forall>x. \<not> P x))"
   "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)"
   "\<exists>x. if x = y then (\<forall>y. y = x \<or> y \<noteq> x) else (\<forall>y. y = (x, x) \<or> y \<noteq> (x, x))"
   "\<exists>x. if x = y then (\<exists>y. y = x \<or> y \<noteq> x) else (\<exists>y. y = (x, x) \<or> y \<noteq> (x, x))"
   "(\<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 [[smt_oracle=true]]
   by smt+
 
 lemma
   "(\<exists>! x. P x) \<longrightarrow> (\<exists>x. P x)"
   "(\<exists>!x. P x) \<longleftrightarrow> (\<exists>x. P x \<and> (\<forall>y. y \<noteq> x \<longrightarrow> \<not>P y))"

   "-(x::real) < 0 \<longleftrightarrow> x > 0"
   "x > 0 \<longrightarrow> -x < 0"
   "x < 0 \<longrightarrow> -x > 0"
   by smt+
 
-lemma 
+lemma
   "(x::real) - 0 = x"
   "0 - x = -x"
   "x < y \<longrightarrow> x - y < 0"
   "x - y = -(y - x)"
   "x - y = -y + x"