--- a/src/FOL/ex/Intuitionistic.thy Thu Jan 03 22:19:19 2019 +0100
+++ b/src/FOL/ex/Intuitionistic.thy Thu Jan 03 22:30:41 2019 +0100
@@ -26,7 +26,7 @@
Therefore $\neg P$ is classically provable iff it is intuitionistically
provable.
-Proof: Let $Q$ be the conjuction of the propositions $A\vee\neg A$, one for
+Proof: Let $Q$ be the conjunction of the propositions $A\vee\neg A$, one for
each atom $A$ in $P$. Now $\neg\neg Q$ is intuitionistically provable because
$\neg\neg(A\vee\neg A)$ is and because double-negation distributes over
conjunction. If $P$ is provable classically, then clearly $Q\rightarrow P$ is