aboutsummaryrefslogtreecommitdiff
path: root/html/features.html
diff options
context:
space:
mode:
authorDavid Aspinall2001-09-03 10:44:21 +0000
committerDavid Aspinall2001-09-03 10:44:21 +0000
commit3c8a94d1f6fb0dc628466ac431d1d6a753ab20dc (patch)
treeecb0cad9505d9b714c576c88b0e2c63bb3b099b8 /html/features.html
parente2383e29558ed59085c17569fab010a34bcfc824 (diff)
Mention hiding proofs.
Diffstat (limited to 'html/features.html')
-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