# HG changeset patch
# User wenzelm
# Date 1546551041 -3600
# Node ID cc6a21413f8a8bb65830a94f852fa7e883d23de5
# Parent  e65314985426a22f1800061f45f4cd57a8f1e8ae
tuned spelling;

diff -r e65314985426 -r cc6a21413f8a src/FOL/ex/Intuitionistic.thy
--- 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