--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/README Wed Dec 21 12:53:45 1994 +0100
@@ -0,0 +1,50 @@
+ Tools: Shell scripts and utilities associated with Isabelle
+
+To make these tools visible, you may wish to add this directory to your PATH
+variable.
+
+
+This directory includes scripts for building Isabelle:
+ make-all shell script for building entire system
+ make-all-poly sample make-all invocation for Poly/ML
+ make-all-nj sample make-all invocation for SML of NJ
+
+
+Also scripts for running Isabelle:
+ xlisten shell script for running Isabelle under X
+ teeinput shell script to run Isabelle, logging inputs to a file
+
+ xlisten and teeinput constitute a *very* primitive user interface.
+ xlisten sets up a window running Isabelle, with a separate small
+ "listener" window, which keeps a log of all input lines. If you are
+ not running the X Window System, teeinput can still be used to record
+ the log. David Aspinall's Emacs-based interface is infinitely better
+ than this one!
+
+
+And scripts to operate on source files (mainly for maintaining compatibility)
+ agrep search for a string throughout all the sources
+ expandshort shell script to expand "shortcuts" in files
+ change_simp shell script to help convert sources to new simplifier
+ conv-theory-files.pl perl script to rename old theory files
+
+ The command
+ conv-theory-files.pl | grep mv
+ generates commands to rename all theory files in a directory hierarchy.
+ See conv-theory-files.pl for more information.
+
+
+And a program to insert calls to the new qed functions
+ qed.cc the program
+ qed.doc its documentation
+ Makefile its Makefile
+ runqed script for bulk changes
+
+ These allow you to update old sources to take advantage of the
+ new database of theorems. They replace calls to result, prove_goal,
+ etc. by calls to functions that store the theorems in the database.
+ The result may fail if the theorems are declared within a structure
+ body, or if they are proved in an ad-hoc union of theories.
+
+
+$Id$