From a98ab308f0d5ab328700478d4fe9579535d12fbd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 30 Nov 2016 22:41:38 +0100
Subject: [PATCH] Document `>` spec pattern.

---
 ProofMode.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/ProofMode.md b/ProofMode.md
index 072512cc8..1ec85aae0 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -232,6 +232,9 @@ _specification patterns_ to express splitting of hypotheses:
 - `>[H1 ... Hn]` : same as the above pattern, but can only be used if the goal
   is a modality, in which case the modality will be kept in the generated goal
   for the premise will be wrapped into the modality.
+- `>[-H1 ... Hn]`  : negated form of the above pattern.
+- `>` : shorthand for `>[-]` (typically used for the last premise of an applied
+  lemma).
 - `[#]` : This pattern can be used when eliminating `P -★ Q` with `P`
   persistent. Using this pattern, all hypotheses are available in the goal for
   `P`, as well the remaining goal.
-- 
GitLab