src/Tools/README

Tools description, largely taken from ../README

	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$