Renamed texinfo file.

1 files changed, 0 insertions, 516 deletions

diff --git a/doc/proof.texinfo b/doc/proof.texinfo
deleted file mode 100644
index 4f886c1d..00000000
--- a/doc/proof.texinfo
+++ /dev/null
@@ -1,516 +0,0 @@
-\input texinfo   @c -*-texinfo-*-
-@c
-@c $Id$
-@c
-@c %**start of header
-@setfilename proof.info
-@settitle Proof General Version 2.0
-@paragraphindent 0
-@c %**end of header
-
-@setchapternewpage odd
-
-@titlepage
-@sp 10
-@comment The title is printed in a large font.
-@center @titlefont{Proof General Version 2.0}
-@sp 2
-@center Organise your proofs with Emacs!
-@sp 2
-@center D. Aspinall, H. Goguen, T. Kleymann and D. Sequeira
-@sp 1
-@center LFCS Edinburgh
-
-
-@c The following two commands start the copyright page.
-@page
-@vskip 0pt plus 1filll
-Copyright @copyright{} 1997, 1998 LEGO Team, LFCS Edinburgh
-@end titlepage
-
-@node    Top, Introduction, (dir), (dir)
-@comment node-name, next,          previous, up
-
-@b{Proof General} is a generic Emacs interface for proof assistants. It
-works ideally under XEmacs 20.4, but can also be used with Emacs 19.34.
-It is supplied ready-customised for these proof assistants:
-
-@itemize @bullet
-@item 
-@b{LEGO Proof General} for LEGO Version 1.3.1 (full support)@*
-by Thomas Kleymann and Dilip Sequeira
-@item 
-@b{Coq Proof General} for Coq Version 6.2 (full support)@*
-by Healfdene Goguen
-@item 
-@b{Isabelle Proof General} for Isabelle (preliminary support)@*
-by David Aspinall
-@end itemize
-
-Proof General itself was written by the above with help from Yves Bertot
-and using ideas from Projet CROAP. 
-
-Proof General is suitable for use by pacifists and Emacs lovers alike.
-
-The code for this Emacs mode is designed to be generic, so you can adapt
-the mode to other proof assistants if you know a little bit of Emacs
-Lisp. Please feel free to download Proof General to customize it for
-another system, and tell us how you get on.
-
-@menu
-* Introduction::          Introduction to Script Management
-* Commands::              Proof mode Commands
-* Multiple Files::        Proof developments spanning several files
-* Proof by Pointing::     Proof using the Mouse
-* An Active Terminator::  Active Terminator minor mode
-* Walkthrough::           An example of using proof mode
-* LEGO mode::             Extra Bindings for LEGO
-* Coq mode::              Extra Bindings for Coq
-* Internals::             The Seedy Underside of Proof mode
-* Known Problems::        Caveat Emptor
-@end menu
-
-@node Introduction, Commands, Top, Top
-@comment node-name, next,          previous, up
-@unnumberedsec Introduction
-
-A @strong{Script Buffer} is the primary buffer for developing proof
-scripts. Its major mode is @emph{proof mode}. A script buffer is divided
-into three regions:
-
-@itemize @bullet
-@item The @emph{Locked} region appears in blue (underlined on monochrome
-displays) and contains commands which have been sent to the proof process
-and verified. The commands in the locked region cannot be edited.
-
-@item The @emph{Queue} region appears in pink (inverse video) and contains
-commands waiting to be sent to the proof process. Like those in the
-locked region, these commands can't be edited.
-
-@item The @emph{Editing} region contains the commands the user is working
-on, and can be edited as normal Emacs text.
-@end itemize
-
-These three regions appear in the buffer in the order above; that is,
-the locked region is always at the start of the buffer, and the editing
-region always at the end. The queue region only exists if there is input
-waiting to be sent to the proof process.
-
-Proof mode has two operations which transfer commands between these
-regions: assertion and retraction. These cause commands to be sent to
-the proof process. The @emph{Process Buffer} records the complete
-communication between the prover and the Script Buffers. Error messages
-and other important messages are highlighted in the Process Buffer. The
-current proof obligations (if any) are always visible in the @emph{Goals
-Buffer}.
-
-Proof General is generous. It is not a perfect interface and users may
-occasionaly want to freely interact with the prover without being
-watched over by the Proof General. Users may interact @emph{directly}
-with the prover by entering text in the Process Buffer instead of
-invoking commands in a Script Buffer. Proof mode supports a variety of
-means to interact with the prover. Try these first!
-
-
-
-
-@strong{Assertion} causes commands from the editing region to be
-transferred to the queue region and sent one by one to the proof
-process. If the command is accepted, it is transferred to the locked
-region, but if an error occurs it is signalled to the user, and the
-offending command is transferred back to the editing region together
-with any remaining commands in the queue.  @strong{Retraction} causes
-commands to be transferred from the locked region to the editing region
-(again via the queue region) and the appropriate 'undo' commands to be
-sent to the proof process.
-
-As commands are transferred to the locked region, they are aggregated
-into segments which constitute the smallest units which can be
-undone. Typically a segment consists of a declaration or definition, or
-all the text from a `goal' command to the corresponding `save' command,
-or the individual commands in the proof of an unfinished goal.  As the
-mouse moves over the the region, the segment containing the pointer will
-be highlighted.
-
-Commands in the editing region can be freely edited while
-commands in the queue are transferred to the proof process. However,
-assertion and retraction commands can only be issued when the queue is
-empty.
-
-@node Commands, Multiple Files, Introduction, Top
-@unnumberedsec Proof Mode Commands
-
-@table @kbd
-
-@item C-c C-b
-assert the commands in the buffer.
-
-@item C-c return
-assert the commands in the editing region up to and
-including the one containing the point.
-
-@item C-c u
-retract the segments in the locked region back to and
-including the one containing the point. If point is outside the *Locked*
-region, the last segment is undone.
-
-@item C-c C-u
-retract the last segment in the locked region, and kill the text in it.
-@footnote{Be careful with this, as it may delete more than you anticipate.
-However, you can always recover the killed text using Emacs Undo.}
-
-@item C-c '
-move the point to the end of the locked region.  If you are in a script
-buffer other than the active scripting buffer, this will also transfer
-you to the active one.
-
-@item C-c C-e
-move the point to the next terminator
-
-@item C-c C-p
-display the proof state in the goals buffer
-
-@item C-c c
-display the context in the process buffer
-
-@item C-c h
-print proof-system specific help text in the process buffer
-
-@item C-c C-c
-interrupt the process. This may leave script management or the
-proof process (or both) in an inconsistent state.
-
-@item C-c C-z
-move the end of the locked region backwards to the end of the segment
-containing the point. @footnote{Don't try this one at home, kids.}
-
-@item C-c C-t
-Send the command at the point to the subprocess, not
-recording it in the locked region. @footnote{This is supplied in order
-to enable the user to test the types and values of expressions. There's
-some checking that the command won't change the proof state, but it
-isn't foolproof.}
-
-@item C-c C-v
-Request a command from the minibuffer and send it to
-the subprocess. Currently no checking whatsoever is done on the command.
-@end table
-
-The command @code{proof-restart-script} can be used to completely
-restart script management.
-
-
-@node Multiple Files, An Active Terminator, Commands, Top
-@unnumberedsec Multiple Files
-
-Proof mode has a rudimentary facility for operating with multiple files
-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?'' 
-if Emacs doesn't think the file is already part of the proof development
-@item ``Reprocess this file?'' 
-if Emacs thinks the file is already included in the proof process. If
-the user confirms, Emacs will cause the proof process to forget the
-contents of the file, so that it is processed afresh.
-@end itemize
-
-Currently this facility requires each script buffer to have a
-corresponding file.
-
-When working with script management in multiple buffers, it is easy
-to lose track of which buffer is the current script buffer. As a mnemonic
-aid, the word @samp{Scripting} appears in the minor mode list of the
-active scripting buffer.
-
-Caveats:
-@itemize @minus
-@item Note that if processing a buffer causes other files to be loaded 
-into the LEGO process, those files will be imported from disk rather
-than from any Emacs buffer in which it is being edited, i.e.@: if your
-file is going to be included indirectly, save it.
-
-@item However much you move around the file system in Emacs, the
-LEGOPATH will be the LEGOPATH you started with. No concept of 
-"current directory" is currently supported.
-@end itemize
-
-@node An Active Terminator, Proof by Pointing, Multiple Files, Top
-@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{;}
-for LEGO, @kbd{.} for Coq) outside a comment or quote will cause the
-character to be entered into the buffer, and all the commands in the
-editing region up to the point to be asserted.
-
-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
-@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.}
-
-Proof by pointing is a facility whereby proof commands can be generated
-by using the mouse to select terms. When proving a goal, a summary of
-the current proof state will appear in the goals buffer. By moving
-the mouse over the buffer, the structure of the goal and hypothesis
-terms will be shown by highlighting. 
-
-If a selection is made using the second (usually the middle) mouse
-button, Emacs will generate the appropriate commands, insert them in the
-script buffer, and send them to the proof process. These commands are
-aggregated in the locked region as a single segment, so that a
-mouse-generated command sequence can be retracted with a single
-retraction command.
-
-Further Information about proof by pointing may be found in the paper
-@cite{User Interfaces for Theorem Provers} by Yves Bertot and Laurent
-Thery, to appear in @cite{Information and Computation}, from which
-the following example is taken.
-
-@menu
-* Proof by Pointing Example::          An example using proof by pointing
-@end menu
-
-@node Proof by Pointing Example, ,Proof by Pointing,Proof by Pointing
-
-Suppose we wish to prove the lego term:
-
-@example
-(((p a) \/ (q b))  /\ @{x:Prop@}(p x) -> (q x)) -> (Ex ([x:Prop] q(x)));
-@end example
-
-Asserting this goal will result in the proof state
-
-@example
-?0 : ((p a \/ q b) /\ @{x:Prop@}(p x)->q x)->Ex ([x:Prop]q x)
-@end example
-
-appearing in the goals buffer. Suppose our strategy is to use a 
-case analysis on the disjunction, starting with the @samp{p(a)} subterm.
-Clicking on this term will cause script management to insert the following
-command sequence in the script buffer, and execute it.
-
-@example
-Intros H; Refine H; Intros H0 H1; 
-Refine or_elim H0 Then Intros H2; Try Refine H2; 
-@end example
-
-
-The goals buffer will then read 
-
-@example
-  H : (p a \/ q b) /\ @{x:Prop@}(p x)->q x
-  H0 : p a \/ q b
-  H1 : @{x:Prop@}(p x)->q x
-  H2 : p a
-  ?10 : Ex ([x:Prop]q x)
-@end example
-
-Clicking on the subterm @samp{(p x)} in the hypothesis H1 will instruct
-script management to prove an instance of @samp{(p x)} and deduce the
-corresponding @samp{(q x)}. The commands
-
-@example
-allE H1; intros +1 H3; Refine impl_elim H3; Try Assumption;
-@end example
-
-are inserted and executed, leaving the proof state as
-
-@example
-  H : (p a \/ q b) /\ @{x:Prop@}(p x)->q x
-  H0 : p a \/ q b
-  H1 : @{x:Prop@}(p x)->q x
-  H2 : p a
-  H3 : (p a)->q a
-  ?20 : (q a)->Ex ([x:Prop]q x)
-@end example
-
-Now clicking on the @samp{q x)} subterm in ?20 will prove the subgoal. We are
-left with the other half of the original case analysis:
-
-@example
-  H : (p a \/ q b) /\ @{x:Prop@}(p x)->q x
-  H0 : p a \/ q b
-  H1 : @{x:Prop@}(p x)->q x
-  H2 : q b
-  ?26 : Ex ([x:Prop]q x)
-@end example
-
-Clicking on @samp{q x} proves the goal.
-
-
-
-
-@node Walkthrough, LEGO mode, Proof by Pointing, Top
-@unnumberedsec A Walkthrough
-
-Here's a LEGO example of how script management is used.
-
-First, we turn on active terminator minor mode by typing @kbd{C-c ;}
-Then we enter 
-
-`Module Walkthrough Import lib_logic;'
-
-The command should be lit in pink (or inverse video if you don't have a
-colour display).  As LEGO imports each module, a line will appear in the
-minibuffer showing the creation of context marks. Eventually the
-command should turn blue, indicating that LEGO has successfully
-processed it. Then type (on a separate line if you like)
-
-@samp{Goal bland_commutes: @{A,B:Prop@} (and A B) -> (and B A);}
-
-The goal should be echoed in the goals buffer.
-
-@samp{Intros;}
-
-Whoops! @kbd{C-c C-u} to pretend that didn't happen.
-
-@samp{intros; andI;}
-
-A proof summary will appear in the goals buffer. We could solve the
-goal by pointing now, but we'll stay with the keyboard.
-
-@samp{Refine H; intros; Immed; Refine H; intros; Immed;}
-
-finishes the Goal. 
-
-@samp{Save bland_commutes;}
-
-Moving the mouse pointer over the locked region now reveals that the
-entire proof has been aggregated into a single segment. Suppose we
-decide to call the goal something more sensible. Moving the cursor up
-into the locked region, somewhere between `Goal' and `Save', we enter
-@kbd{C-c u}.  The segment is transferred back into the editing
-region. Now we correct the goal name, move the cursor to the end of the
-buffer, and type @kbd{C-c return}.  Proof mode queues the commands for
-processing and executes them.
-
-@node LEGO mode, Coq mode, Walkthrough, Top
-@unnumberedsec LEGO mode
-
-LEGO mode is a mode derived from proof mode for editing LEGO scripts.
-There are some abbreviations for common commands, which
-add text to the buffer:
-
-@table @kbd
-@item C-c i   
-intros
-@item C-c I   
-Intros
-@item C-c R   
-Refine
-@end table
-
-
-@node Coq mode, Known Problems, LEGO mode, Top
-@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:
-
-@table @kbd
-
-@item C-c C-s
-search for items in the library of a given type.  This runs the
-@kbd{Search} command of Coq.
-
-@end table
-
-In addition, there are some abbreviations for common commands, which
-add text to the buffer:
-
-@table @kbd
-@item C-c I   
-Intros
-@item C-c a
-Apply
-@end table
-
-@node Known Problems, Internals, Coq mode, Top
-@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
-become distressed, and may eventually sulk. In such instances
-@code{proof-restart-script-management} may be of use.
-
-A few things to avoid: 
-
-@itemize @minus
-@item If you're using script management with multiple files, don't start
-changing the file names.
-
-@item Script Management doesn't understand how to undo @code{Discharge}
-commands in LEGO, and any attempts it makes to do so may leave it in an
-inconsistent state. If you're undoing the effects of a @code{Discharge}
-command, retract back to the declaration of whatever gets discharged.
-
-@item Proof by Pointing doesn't work very well, and is inefficiently
-implemented. 
-
-@item The locked and queue regions are not quite read-only: in particular 
-Emacs Undo can insert text into them. 
-
-@item When a LEGO import command fails, the created "Mark" is not
-forgotten, and the proof process thinks the file has been included. So
-if you assert the command again, it will probably be accepted by LEGO,
-because the relevant mark is in the namespace.
-@end itemize
-
-Fixes for some of these may be provided in a future release.
-
-@node Internals,  Adding New Proof Assistant, Known Problems, Top
-@unnumberedsec Internals
-
-@menu
-* Adding New Proof Assistant:: 
-* Literature::                  
-@end menu
-
-@node Adding New Proof Assistant, Literature, Internals, Internals
-@comment  node-name,  next,  previous,  up
-@unnumberedsubsec Adding Support for a New Proof Assistant
-
-Suppose your new assistant is
-called myassistant.
-
-@itemize @minus
-@item Make a directory myassistant to put the specific customization and associated files in,
-  called myassistant
-@item Edit proof-site.el to add a new case to the 'proof-assistant' variable.
-@end itemize
-
-@node Literature, ,Adding New Proof Assistant, Internals
-@comment  node-name,  next,  previous,  up
-@unnumberedsubsec Literature
-
-The current version supports Script Management as documented in: 
-
-@itemize @bullet
-@item
-Yves Bertot and Laurent Th@'ery. A generic approach to building
-user interfaces for theorem provers. To appear in Journal of
-Symbolic Computation.
-@end itemize
-
-It has the beginnings of support for Proof by Pointing, as documented in: 
-
-@itemize @bullet
-@item
-Yves Bertot, Thomas Kleymann-Schreiber and Dilip Sequeira. Implementing
-Proof by Pointing without a
-Structure Editor. LFCS Technical Report ECS-LFCS-97-368. Also published as Rapport de recherche de
-l'INRIA Sophia Antipolis RR-3286 
-@end itemize
-
-
-
-
-
-@bye