diff options
| author | Landon D. C. Elkind | 2021-02-03 16:04:24 -0700 |
|---|---|---|
| committer | GitHub | 2021-02-03 16:04:24 -0700 |
| commit | 48167a7aee5f5fbac6761468d0e59fb3d97020cf (patch) | |
| tree | fa8b69000c9072cea7bb274375f2d2f2945efa2e /PL.v | |
| parent | 0ccdbb2a6924041f697484a555557328f0d77d9b (diff) | |
PL prettified further
Diffstat (limited to 'PL.v')
| -rw-r--r-- | PL.v | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -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*) |