From bcc5f396ded2d1782468bab5d9f4859bf9697172 Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Mon, 1 Apr 2024 13:44:26 -0500
Subject: [PATCH] Extra sentence about assumes in subproofs

---
 spec/doc.tex | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/spec/doc.tex b/spec/doc.tex
index c354011..c55ef52 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -808,9 +808,12 @@ A subproof is concluded by a matching \inlineAlethe{step} command.  This step mu
 a \index{rule!concluding}{\em concluding rule}
 (such as \proofRule{subproof}, \proofRule{bind}, and so forth).
 
-After the \inlineAlethe{anchor} command, the proof uses \inlineAlethe{assume} commands to list
-the assumptions of the subproof.  Subsequently, the subproof is a list of
-\inlineAlethe{step} commands that can use prior steps in the subproofs as premises.
+After the \inlineAlethe{anchor} command, the proof uses
+\inlineAlethe{assume} commands to list the assumptions of the subproof.
+Subsequently, the subproof is a list of \inlineAlethe{step} commands
+that can use prior steps in the subproofs as premises.  It is not allowed
+to issue \inlineAlethe{assume} commands after the first \inlineAlethe{step}
+command of a subproof has been issued.
 
 In the abstract notation, every step is associated with a context.  The
 concrete syntax uses anchors to optimize this.
-- 
GitLab