aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--html/features.html6
1 files changed, 4 insertions, 2 deletions
diff --git a/html/features.html b/html/features.html
index cc38adde..5a5e3a98 100644
--- a/html/features.html
+++ b/html/features.html
@@ -23,8 +23,10 @@ you'd like an interface with the following features...
assistant. Parts of a proof script that have been processed are
displayed in blue and are "locked" -- they cannot be edited. Parts
of the script currently being processed by the proof assistant are
- shown in red. Proof General has commands for processing new parts
- of the buffer, or undoing already processed parts.
+ shown in red. Bodies of completed proofs in the locked region
+ can be hidden from view to help browsing.
+ Proof General has commands for processing new parts
+ of the buffer, or undoing already processed parts.
</p>
<p>
Take a look at these