From a08d25d6a9ff600a5aa21647ae49dd99219c6d6d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= <marko@dimjasevic.net>
Date: Wed, 30 Jan 2019 16:30:01 +0100
Subject: [PATCH] Connectives: changes a punctuation before a code block

---
 src/plfa/Connectives.lagda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/plfa/Connectives.lagda b/src/plfa/Connectives.lagda
index 64f04264..118615c2 100644
--- a/src/plfa/Connectives.lagda
+++ b/src/plfa/Connectives.lagda
@@ -450,7 +450,7 @@ paradoxical situation.  Given evidence that `⊥` holds, we might
 conclude anything!  This is a basic principle of logic, known in
 medieval times by the Latin phrase _ex falso_, and known to children
 through phrases such as "if pigs had wings, then I'd be the Queen of
-Sheba".  We formalise it as follows.
+Sheba".  We formalise it as follows:
 \begin{code}
 ⊥-elim : ∀ {A : Set}
   → ⊥