diff options
| author | Hugo Herbelin | 2019-10-14 12:58:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-10-14 12:59:16 +0200 |
| commit | b13c438c78539040f8adf67f0b92a8f31e2e8c9f (patch) | |
| tree | ab5cdef48c7cc85e36139c325b47e67428216882 | |
| parent | a8166315acaa63252f5753b71ad26d126873bbe4 (diff) | |
ClassicalFacts.v: Unifying format for bibliographical references.
| -rw-r--r-- | theories/Logic/ClassicalFacts.v | 6 |
1 files 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). |