diff -r 83b5911c0164 -r 75f5c63f6cfa src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Tue Oct 27 16:59:44 2020 +0000
+++ b/src/HOL/SMT.thy	Wed Oct 28 08:41:07 2020 +0100
@@ -250,7 +250,8 @@
   by auto
 
 lemma verit_and_pos:
-  \<open>(a \<Longrightarrow> \<not>b \<or> A) \<Longrightarrow> \<not>(a \<and> b) \<or> A\<close>
+  \<open>(a \<Longrightarrow> \<not>(b \<and> c) \<or> A) \<Longrightarrow> \<not>(a \<and> b \<and> c) \<or> A\<close>
+  \<open>(a \<Longrightarrow> b \<Longrightarrow> A) \<Longrightarrow> \<not>(a \<and> b) \<or> A\<close>
   \<open>(a \<Longrightarrow> A) \<Longrightarrow> \<not>a \<or> A\<close>
   \<open>(\<not>a \<Longrightarrow> A) \<Longrightarrow> a \<or> A\<close>
   by blast+
@@ -276,9 +277,10 @@
   by auto
 
 lemma verit_and_neg:
-  \<open>B \<or> B' \<Longrightarrow> (A \<and> B) \<or> \<not>A \<or> B'\<close>
-  \<open>B \<or> B' \<Longrightarrow> (\<not>A \<and> B) \<or> A \<or> B'\<close>
-  by auto
+  \<open>(a \<Longrightarrow> \<not>b \<or> A) \<Longrightarrow> \<not>(a \<and> b) \<or> A\<close>
+  \<open>(a \<Longrightarrow> A) \<Longrightarrow> \<not>a \<or> A\<close>
+  \<open>(\<not>a \<Longrightarrow> A) \<Longrightarrow> a \<or> A\<close>
+  by blast+
 
 lemma verit_forall_inst:
   \<open>A \<longleftrightarrow> B \<Longrightarrow> \<not>A \<or> B\<close>