Tools description, largely taken from ../README
Wed, 21 Dec 1994 12:53:45 +0100
changeset 817 99824db26a29
parent 816 2f89be458be5
child 818 0b9ec0374bfd
Tools description, largely taken from ../README
--- /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
+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
+  perl script to rename old theory files
+	The command
+ | grep mv
+	generates commands to rename all theory files in a directory hierarchy.
+	See for more information.
+And a program to insert calls to the new qed functions
+		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.