changeset 69591 cc6a21413f8a
parent 69590 e65314985426
child 69593 3dda49e08b9d
--- 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
-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