--- a/src/FOL/ex/Intuitionistic.thy Sat Apr 02 17:03:35 2022 +0000
+++ b/src/FOL/ex/Intuitionistic.thy Sun Apr 03 14:48:55 2022 +0100
@@ -65,6 +65,14 @@
\<longrightarrow> (((F \<longrightarrow> A) \<longrightarrow> B) \<longrightarrow> I) \<longrightarrow> E\<close>
by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
+text \<open>Admissibility of the excluded middle for negated formulae\<close>
+lemma \<open>(P \<or> \<not>P \<longrightarrow> \<not>Q) \<longrightarrow> \<not>Q\<close>
+ by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
+
+text \<open>The same in a more general form, no ex falso quodlibet\<close>
+lemma \<open>(P \<or> (P\<longrightarrow>R) \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> Q \<longrightarrow> R\<close>
+ by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
+
subsection \<open>Lemmas for the propositional double-negation translation\<close>