summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorLandon D. C. Elkind2021-02-03 16:04:24 -0700
committerGitHub2021-02-03 16:04:24 -0700
commit48167a7aee5f5fbac6761468d0e59fb3d97020cf (patch)
treefa8b69000c9072cea7bb274375f2d2f2945efa2e
parent0ccdbb2a6924041f697484a555557328f0d77d9b (diff)
PL prettified further
-rw-r--r--PL.pdfbin436367 -> 420430 bytes
-rw-r--r--PL.v2
2 files changed, 1 insertions, 1 deletions
diff --git a/PL.pdf b/PL.pdf
index 57914c0..7fe64e3 100644
--- a/PL.pdf
+++ b/PL.pdf
Binary files differ
diff --git a/PL.v b/PL.v
index 9809b74..687fd9b 100644
--- a/PL.v
+++ b/PL.v
@@ -15,7 +15,7 @@ Axiom Impl1_01 : ∀ P Q : Prop,
Axiom MP1_1 : ∀ P Q : Prop,
(P → Q) → P → Q. (*Modus ponens*)
- (**1.11 ommitted: it is MP for propositions
+ (*1.11 ommitted: it is MP for propositions
containing variables. Likewise, ommitted
the well-formedness rules 1.7, 1.71, 1.72*)