From a8166315acaa63252f5753b71ad26d126873bbe4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 14 Oct 2019 12:54:31 +0200
Subject: Weak excluded-middle: adding a reference.

---
 theories/Logic/ClassicalFacts.v | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index 98dcd0d122..9ba3db6eff 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -523,11 +523,15 @@ End Weak_proof_irrelevance_CCI.
 (** ** Weak excluded-middle *)
 
 (** The weak classical logic based on [~~A \/ ~A] is referred to with
-    name KC in [[ChagrovZakharyaschev97]]
+    name KC in [[ChagrovZakharyaschev97]]. See [[SorbiTerwijn11]] for
+    a short survey.
 
    [[ChagrovZakharyaschev97]] Alexander Chagrov and Michael
    Zakharyaschev, "Modal Logic", Clarendon Press, 1997.
-*)
+
+   [[SorbiTerwijn11]] Andrea Sorbi and Sebastiaan A. Terwijn,
+   "Generalizations of the weak law of the excluded-middle", Notre
+   Dame J. Formal Logic, vol 56(2), pp 321-331, 2015. *)
 
 Definition weak_excluded_middle :=
   forall A:Prop, ~~A \/ ~A.
-- 
cgit v1.2.3