From 3661528d9dbcbdb9b4ebbdac6d491b3e1f73c376 Mon Sep 17 00:00:00 2001
From: Thomas Kleymann
Date: Fri, 14 Aug 1998 10:52:07 +0000
Subject: *** empty log message ***

---
 script-management.texinfo | 30 +++++++++++++++---------------
 1 file changed, 15 insertions(+), 15 deletions(-)

diff --git a/script-management.texinfo b/script-management.texinfo
index 7cd401eb..6ca81ed7 100644
--- a/script-management.texinfo
+++ b/script-management.texinfo
@@ -43,7 +43,7 @@ modes exist for LEGO and Coq.
 
 @node Credits, Introduction, Top, Top
 @comment node-name, next,          previous, up
-@section Credits
+@unnumberedsec Credits
 
 Inspired by Yves Bertot's Centaur-based proof environment CtCoq, Healf
 Goguen, Thomas Kleymann and Dilip Sequeira have implented a generic
@@ -53,7 +53,7 @@ Sequeira.
 
 @node Introduction, Commands, Credits, Top
 @comment node-name, next,          previous, up
-@section Introduction
+@unnumberedsec Introduction
 
 Each script resides in an Emacs buffer, called a @emph{script buffer},
 which is divided into three regions:
@@ -105,7 +105,7 @@ assertion and retraction commands can only be issued when the queue is
 empty.
 
 @node Commands, Multiple Files, Introduction, Top
-@section Proof Mode Commands
+@unnumberedsec Proof Mode Commands
 
 @table @kbd
 
@@ -141,7 +141,7 @@ display the proof state in the response buffer
 display the context in the response buffer
 
 @item C-c h
-print LEGO help text in the response buffer
+print proof-system specific help text in the response buffer
 
 @item C-c C-c
 interrupt the process process. This may leave script management or the
@@ -168,12 +168,12 @@ restart script management.
 
 
 @node Multiple Files, An Active Terminator, Commands, Top
-@section Multiple Files
+@unnumberedsec Multiple Files
 
 Proof mode has a rudimentary facility for operating with multiple files
-in a LEGO proof development. If the user invokes script management in a
-different buffer from the one in which it is running, one of two prompts
-will appear:
+in a proof development. This is currently only supported for LEGO. If
+the user invokes script management in a different buffer from the one in
+which it is running, one of two prompts will appear:
 
 @itemize @bullet
 @item ``Steal script management?'' 
@@ -205,7 +205,7 @@ LEGOPATH will be the LEGOPATH you started with. No concept of
 @end itemize
 
 @node An Active Terminator, Proof by Pointing, Multiple Files, Top
-@section An Active Terminator
+@unnumberedsec An Active Terminator
 
 Proof mode has a minor mode which causes the terminator to become
 active. When this mode is active, pressing the terminator key (@kbd{;}
@@ -217,7 +217,7 @@ This mode can be toggled with the command
 `proof-active-terminator-minor-mode' (@kbd{C-c ;} or @kbd{C-c .})
 
 @node Proof by Pointing, Walkthrough, An Active Terminator, Top
-@section Proof by Pointing
+@unnumberedsec Proof by Pointing
 
 @emph{This mode is currently very unreliable, and we do not guarantee
 that it will work as discussed in this document.}
@@ -315,7 +315,7 @@ Clicking on @samp{q x} proves the goal.
 
 
 @node Walkthrough, LEGO mode, Proof by Pointing, Top
-@section A Walkthrough
+@unnumberedsec A Walkthrough
 
 Here's a LEGO example of how script management is used.
 
@@ -359,7 +359,7 @@ buffer, and type @kbd{C-c return}.  Proof mode queues the commands for
 processing and executes them.
 
 @node LEGO mode, Coq mode, Walkthrough, Top
-@section LEGO mode
+@unnumberedsec LEGO mode
 
 LEGO mode is a mode derived from proof mode for editing LEGO scripts.
 There are some abbreviations for common commands, which
@@ -376,7 +376,7 @@ Refine
 
 
 @node Coq mode, Known Problems, LEGO mode, Top
-@section Coq mode
+@unnumberedsec Coq mode
 
 Coq mode is a mode derived from proof mode for editing Coq scripts.
 As well as custom popup menus, it has the following commands:
@@ -400,7 +400,7 @@ Apply
 @end table
 
 @node Known Problems, Internals, Coq mode, Top
-@section Known Problems
+@unnumberedsec Known Problems
 
 Since Emacs is pretty flexible, there are a whole bunch of things you
 can do to confuse script management. When it gets confused, it may
@@ -433,7 +433,7 @@ because the relevant mark is in the namespace.
 Fixes for some of these may be provided in a future release.
 
 @node Internals,  , Known Problems, Top
-@section Internals
+@unnumberedsec Internals
 
 I may one day document the script management internals here. Until then,
 UtSL.
-- 
cgit v1.2.3