From 7d30ec0480740b1ebaa9ce350badae58171d3470 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 5 Jul 2016 18:20:22 +0200
Subject: [PATCH] Fix typo.
---
ProofMode.md | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/ProofMode.md b/ProofMode.md
index d86362ea8..834e8ef3b 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -122,7 +122,7 @@ appear at the top level:
- `>` : introduce a later (which strips laters from all hypotheses).
- `{H1 ... Hn}` : clear `H1 ... Hn`.
- `{$H1 ... $Hn}` : frame `H1 ... Hn` (this pattern can be mixed with the
- previous pattern, e.g., `{$H1 H2 #H3}`).
+ previous pattern, e.g., `{$H1 H2 $H3}`).
- `/=` : perform `simpl`.
- `*` : introduce all universal quantifiers.
- `**` : introduce all universal quantifiers, as well as all arrows and wands.
--
GitLab