diff -r 173667d73115 -r 4eb98849c5c0 src/HOL/SMT_Examples/SMT_Tests.thy
--- 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"