From adf060c19e075726c5c56c2ca9410cf35b58b569 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 23 Jan 2017 18:09:42 +0100
Subject: [PATCH] simplify doc

---
 ProofMode.md | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/ProofMode.md b/ProofMode.md
index b17ec1fc6..3e3f9c429 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -18,8 +18,7 @@ Applying hypotheses and lemmas
   proof mode terms below.
   If the applied term has more premises than given specialization patterns, the
   pattern is extended with `[] ... []`.  As a consequence, all unused spatial
-  hypotheses move to the last premise without an explicit specialization
-  pattern.
+  hypotheses move to the last premise.
 
 Context management
 ------------------
-- 
GitLab