author wenzelm Thu, 03 Jan 2019 22:30:41 +0100 changeset 69591 cc6a21413f8a parent 69590 e65314985426 child 69592 a80d8ec6c998
tuned spelling;
--- 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