# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1648993735 -3600
# Node ID 970b9ab6c439f5b0de8d83485ec7e900ed757949
# Parent  cdf84288d93c4ca134eb15df94f1f5793b5b5c9c
two new examples

diff -r cdf84288d93c -r 970b9ab6c439 src/FOL/ex/Intuitionistic.thy
--- 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>