--- a/src/HOL/SMT_Examples/SMT_Tests.thy Mon Jul 12 22:35:41 2010 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy Tue Jul 13 02:29:05 2010 +0200
@@ -84,6 +84,7 @@
lemma
"case P of True \<Rightarrow> P | False \<Rightarrow> \<not>P"
+ "case P of False \<Rightarrow> \<not>P | True \<Rightarrow> P"
"case \<not>P of True \<Rightarrow> \<not>P | False \<Rightarrow> P"
"case P of True \<Rightarrow> (Q \<longrightarrow> P) | False \<Rightarrow> (P \<longrightarrow> Q)"
by smt+
@@ -176,6 +177,11 @@
by smt+
lemma
+ "(\<forall>x\<in>M. P x) \<and> c \<in> M \<longrightarrow> P c"
+ "(\<exists>x\<in>M. P x) \<or> \<not>(P c \<and> c \<in> M)"
+ by smt+
+
+lemma
"let P = True in P"
"let P = P1 \<or> P2 in P \<or> \<not>P"
"let P1 = True; P2 = False in P1 \<and> P2 \<longrightarrow> P2 \<or> P1"