|
1 Tools: Shell scripts and utilities associated with Isabelle |
|
2 |
|
3 To make these tools visible, you may wish to add this directory to your PATH |
|
4 variable. |
|
5 |
|
6 |
|
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 |
|
11 |
|
12 |
|
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 |
|
16 |
|
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! |
|
23 |
|
24 |
|
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 conv-theory-files.pl perl script to rename old theory files |
|
30 |
|
31 The command |
|
32 conv-theory-files.pl | grep mv |
|
33 generates commands to rename all theory files in a directory hierarchy. |
|
34 See conv-theory-files.pl for more information. |
|
35 |
|
36 |
|
37 And a program to insert calls to the new qed functions |
|
38 qed.cc the program |
|
39 qed.doc its documentation |
|
40 Makefile its Makefile |
|
41 runqed script for bulk changes |
|
42 |
|
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. |
|
48 |
|
49 |
|
50 $Id$ |