diff options
| author | Thomas Kleymann | 1998-08-14 10:09:58 +0000 |
|---|---|---|
| committer | Thomas Kleymann | 1998-08-14 10:09:58 +0000 |
| commit | 384dea58f73d89d64688183a4be55a4267184636 (patch) | |
| tree | ae534f3cf539fb3876655f7bc191aac843dcc9a9 | |
| parent | 8549abf870767f9dbc11fd92e0c1ad1126cd3dfb (diff) | |
*** empty log message ***
| -rw-r--r-- | script-management.texinfo | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/script-management.texinfo b/script-management.texinfo index 268add70..7cd401eb 100644 --- a/script-management.texinfo +++ b/script-management.texinfo @@ -18,7 +18,7 @@ Copyright @copyright{} 1997, 1998 LEGO Team, LFCS Edinburgh @end titlepage -@node Top, Introduction, (dir), (dir) +@node Top, Credits, (dir), (dir) @comment node-name, next, previous, up A @emph{proof script} is a sequence of commands to a proof assistant. @@ -42,6 +42,7 @@ modes exist for LEGO and Coq. @end menu @node Credits, Introduction, Top, Top +@comment node-name, next, previous, up @section Credits Inspired by Yves Bertot's Centaur-based proof environment CtCoq, Healf @@ -50,7 +51,8 @@ proof mode for Emacs. The original proof-by-pointing algorithm has been implemented by Yves Bertot. This manual was originally written by Dilip Sequeira. -@node Introduction, Credits, Commands, Top +@node Introduction, Commands, Credits, Top +@comment node-name, next, previous, up @section Introduction Each script resides in an Emacs buffer, called a @emph{script buffer}, |