Renamed file

1 files changed, 0 insertions, 196 deletions

diff --git a/doc/notes.txt b/doc/notes.txt
deleted file mode 100644
index 0cf83b88..00000000
--- a/doc/notes.txt
+++ /dev/null
@@ -1,196 +0,0 @@
-Developers' Notes about Documentation
--------------------------------------
-
-
-
-
-* Plan for outline of improved documentation.   (Completed)
-
- Terminology:  I suggest "proof mode" should become "proof script
- mode", aka "the proof script mode of Proof General".  We should
- be careful here, e.g. present docs speak of buffers in proof
- mode, etc, but no buffer is directly in that mode, which is
- confusing to the users, at least!
- 
- 1. Introduction						[da]
-	1.1  Quick start guide
-	1.2  Feature list, xref'd to later chaps.
-	1.2  Supported Proof Assistants, xref'd too.
-	      Support for new instances, xref'd to later chaps.
-	
- 2. Basics of script management					[da]
-        
-	2.1  What a proof script is
-	2.2  Locked region and queue region
-	2.3  Script processing commands
-	2.4  Toolbar commands
-        2.5  Other commands
-	2.4  Walkthrough example [maybe in appendix?]
-
- 3. Advanced script management					[done]
-        3.1  Proof General's view of processed files
-	3.2  Switching between proof scripts
-	3.3  Retracting across files
-	3.4  Handy hints and tips  (e.g. C-c C-b stuff?)
-	3.5  Using the proof shell
-	[ 3.6  Re-synchronizing with the proof assistant - if added ]
-
- 4. Customizing Proof General					[da]
-	4.1  Setting user options, what they are:
-	       proof-splash-inhibit
-	       etc.
-        4.2  Using proof assistant on another machine
-	4.3  Examining configuration settings (xref'd later)
-	
- 5. LEGO Proof General						[done]
-	5.1  LEGO commands
-	5.2  LEGO customizations
-	
- 6. Coq Proof General						[anon]
-        6.1  Coq commands
-	6.2  Coq customizations
-
- 7. Isabelle Proof General					[da]
-	7.1  Isabelle commands
-	7.2  Isabelle customizations
-	7.3  Notes about multiple files
-
- 8. Adapting Proof General to New Provers			[da]
-	8.1  Files and directories.  Skeleton code.
-	8.2  Settings for proof scripts
-	8.3  Settings for proof shell
-	     -- Special annotations
-	
- 9. Internals of Proof General.					[tms]
-	9.1  Proof script mode:
-		- fontification hacks
-		- spans in locked region
-	9.2  Proof shell mode
-		- proof-action-list
-		- proof-shell-exec-loop
-		- proof-shell-output-filter
-		- eager annotations
-
- 10. Credits and history					[done]
- 
- APPENDIX
-
- A. Obtaining and installing the software			[da]
- B. Known bugs  						[done]
- C. Future ideas and plans					[da]
- 
- 
-*********
-
-Support for Function Menus
-
-fume-func is a handy package which makes a menu from the function
-declarations in a buffer.  Proof General configures fume-func so
-that you can quickly jump to particular proofs in a script buffer.
-
-If you want to use fume-func, you may need to enable it for
-yourself.  It is distributed with XEmacs (and FSF GNU Emacs)
-but by not enabled by default.  To enable it you should find
-the file func-menu.el and follow the instructions there.  
-At the time of writing, the current version of XEmacs is 20.4 and
-it has these instructions:
-
-(require 'func-menu)
-(define-key global-map 'f8 'function-menu)
-(add-hook 'find-file-hooks 'fume-add-menubar-entry)
-(define-key global-map "\C-cl" 'fume-list-functions)
-(define-key global-map "\C-cg" 'fume-prompt-function-goto)
-(define-key global-map '(shift button3) 'mouse-function-menu)
-(define-key global-map '(meta  button1) 'fume-mouse-function-goto)
-
-If you have any other version of Emacs, you should check the
-fume-func.el file
-
-
-
-*********
-
-
-Isabelle with multiple files.
-
-Proper multiple file support only works for .ML files which are read
-via the theory loader, with use_thy.  If you want to load .ML files
-which aren't associated with theories, it's best to use a dummy
-theory, see [Reference to Isabelle manual]
-
-
-*****************************************************************
-
-Notes for writing a paper describing Proof General
--------------------------------------------------
-
-
-Thesis/introduction
-===================
-
-As programming languages have evolved, environments for developing and
-debugging programs have also improved.  However, discounting various
-"visual" programming languages, a program is usually still a piece of
-text which can be directly edited by a programmer, a situation which
-hasn't changed since the early days when VDUs replaced punched cards.
-
-Similarly, whilst the history of languages for proof assistants is
-much shorter, we believe that a proof script, describing the
-operations needed to construct a proof, will remain the fundamental
-form of input for proof systems.
-
-...
-- interactive proof assistants geared to developing proof scripts
-  interactively, but may not come with integrated editing support.
-  Problem of shell-like interaction is that input has to be
-  tediously reassembled after or during proof to get a successful
-  proof script.
-
-- script management [refs] aims to make this process easier.
-
-
-
-Aspects of design
-=================
-
-- Generic.  Fits inside Emacs architecture.  (Compare with comint).
-
-- Extensive use of Emacs Customization mechanism to make it easy
-  to set/inspect configuration as well as user-options.
-
-- Script management with multiple files
-
-
-Seen one proof assistant, use them all
-======================================
-
-- Same interface for different underlying systems
-
-- Compare: web technology, where "browsing" works for 
-  different protocols: http, ftp, etc
-
-- Anyone can use Proof General to browse and replay proofs from
-  other systems, without needing to know how to invoke
-  the system, etc. 
-
-- However, proof script language and output remains particular to
-  each prover.   It would be another (interesting) project to attempt to
-  map input and output into an interchange format for proof systems.
-
-
-
-A Specification for a proof assistant interface
-===============================================
-
-The settings to instantiate Proof General can be seen as a set of 
-requirements for a proof assistant interface.
-
-
-
-Example of API design guidlines
-===============================
-
-1. Use a different prompt for continued lines during input
-communication.  Helps parsing output.
-
-