--- a/src/HOL/SMT_Examples/SMT_Tests.thy Tue Jan 01 11:35:22 2013 +0100
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy Tue Jan 01 11:36:30 2013 +0100
@@ -109,7 +109,6 @@
"\<forall>x. P x \<longrightarrow> (\<forall>y. P x \<or> P y)"
"(\<forall>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>x. P x) \<and> (\<forall>x. Q x)"
"(\<forall>x. P x) \<or> R \<longleftrightarrow> (\<forall>x. P x \<or> R)"
- "(\<forall>x. P x) \<and> R \<longleftrightarrow> (\<forall>x. P x \<and> R)"
"(\<forall>x y z. S x z) \<longleftrightarrow> (\<forall>x z. S x z)"
"(\<forall>x y. S x y \<longrightarrow> S y x) \<longrightarrow> (\<forall>x. S x y) \<longrightarrow> S y x"
"(\<forall>x. P x \<longrightarrow> P (f x)) \<and> P d \<longrightarrow> P (f(f(f(d))))"
@@ -118,6 +117,11 @@
by smt+
lemma
+ "(\<forall>x. P x) \<and> R \<longleftrightarrow> (\<forall>x. P x \<and> R)"
+ using [[smt_oracle]] by smt
+ (* BUG: Z3 proof parser (line 34): unknown function symbol: "S2!val!0" *)
+
+lemma
"\<exists>x. x = x"
"(\<exists>x. P x) \<longleftrightarrow> (\<exists>y. P y)"
"(\<exists>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>x. P x) \<or> (\<exists>x. Q x)"
@@ -133,7 +137,8 @@
"\<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))"
-by smt+
+ using [[smt_oracle]] by smt+
+ (* BUG: Z3 proof parser (line 34): unknown function symbol: "S2!val!0" *)
lemma
"(\<not>(\<exists>x. P x)) \<longleftrightarrow> (\<forall>x. \<not> P x)"