changeset 817 99824db26a29
child 3279 815ef5848324
equal deleted inserted replaced
816:2f89be458be5 817:99824db26a29
     1 	Tools: Shell scripts and utilities associated with Isabelle
     3 To make these tools visible, you may wish to add this directory to your PATH
     4 variable.
     7 This directory includes scripts for building Isabelle:
     8   make-all		shell script for building entire system
     9   make-all-poly		sample make-all invocation for Poly/ML
    10   make-all-nj		sample make-all invocation for SML of NJ
    13 Also scripts for running Isabelle:
    14   xlisten		shell script for running Isabelle under X
    15   teeinput		shell script to run Isabelle, logging inputs to a file
    17 	xlisten and teeinput constitute a *very* primitive user interface.
    18 	xlisten sets up a window running Isabelle, with a separate small
    19 	"listener" window, which keeps a log of all input lines.  If you are
    20 	not running the X Window System, teeinput can still be used to record
    21 	the log.  David Aspinall's Emacs-based interface is infinitely better
    22 	than this one!
    25 And scripts to operate on source files (mainly for maintaining compatibility)
    26   agrep			search for a string throughout all the sources
    27   expandshort		shell script to expand "shortcuts" in files
    28   change_simp		shell script to help convert sources to new simplifier
    29  perl script to rename old theory files
    31 	The command
    32 | grep mv
    33 	generates commands to rename all theory files in a directory hierarchy.
    34 	See for more information.
    37 And a program to insert calls to the new qed functions
    38		the program
    39   qed.doc		its documentation
    40   Makefile		its Makefile
    41   runqed		script for bulk changes
    43 	These allow you to update old sources to take advantage of the
    44 	new database of theorems.  They replace calls to result, prove_goal,
    45 	etc. by calls to functions that store the theorems in the database.
    46 	The result may fail if the theorems are declared within a structure
    47 	body, or if they are proved in an ad-hoc union of theories.
    50 $Id$