From b13c438c78539040f8adf67f0b92a8f31e2e8c9f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 14 Oct 2019 12:58:26 +0200
Subject: ClassicalFacts.v: Unifying format for bibliographical references.

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

diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index 9ba3db6eff..8538b54c08 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -553,11 +553,11 @@ Definition classical_de_morgan_law :=
 (** [(A->B) \/ (B->A)] is studied in [[Dummett59]] and is based on [[Gödel33]].
 
     [[Dummett59]] Michael A. E. Dummett. "A Propositional Calculus
-    with a Denumerable Matrix", In the Journal of Symbolic Logic, Vol
-    24 No. 2(1959), pp 97-103.
+    with a Denumerable Matrix", In the Journal of Symbolic Logic, vol
+    24(2), pp 97-103, 1959.
 
     [[Gödel33]] Kurt Gödel. "Zum intuitionistischen Aussagenkalkül",
-    Ergeb. Math. Koll. 4 (1933), pp. 34-38.
+    Ergeb. Math. Koll. 4, pp. 34-38, 1933.
  *)
 
 Definition GodelDummett := forall A B:Prop, (A -> B) \/ (B -> A).
-- 
cgit v1.2.3