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$