# HG changeset patch
# User lcp
# Date 788010825 -3600
# Node ID 99824db26a29507ede96510402711947d396bf8d
# Parent  2f89be458be5b695066fb842336ab07b58597df0
Tools description, largely taken from ../README

diff -r 2f89be458be5 -r 99824db26a29 src/Tools/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
+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$