--- a/src/Tools/README Tue Dec 16 12:17:48 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-
-***************************************************************************
-
-IMPORTANT NOTE: These tools will disappear next time!
-
-***************************************************************************
-
-
- 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$
--- a/src/Tools/expandshort Tue Dec 16 12:17:48 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-#! /usr/bin/perl -pi~~
-# $Id$
-#Shell script to expand shorthand goal commands
-# ALSO contracts uses of resolve_tac, dresolve_tac, eresolve_tac,
-# rewrite_goals_tac on 1-element lists
-# [Tabs are forbidden in strings. Use "expand" or "untabify" in emacs".]
-#
-# Usage:
-# expandshort FILE1 ... FILEn
-#
-#Renames old versions of the files as FILE1~~ ... FILEn~~
-#
-s/\bsafe_tac *\(claset *\( *\) *\)/Safe_tac/;
-s/ *\(Safe_tac\) *([0-9]+)/ Safe_tac \1/;
-s/ *\(Safe_tac\)/ Safe_tac/;
-s/\bby\(/by (/;
-s/\bba\b *(\d+);/by (assume_tac \1);/;
-s/\bbr\b *([^;]*) (\d+);/by (rtac \1 \2);/;
-s/\bbrs\b *([^;]*) (\d+);/by (resolve_tac \1 \2);/;
-s/\bbd\b *([^;]*) (\d+);/by (dtac \1 \2);/;
-s/\bbds\b *([^;]*) (\d+);/by (dresolve_tac \1 \2);/;
-s/\bbe\b *([^;]*) (\d+);/by (etac \1 \2);/;
-s/\bbes\b *([^;]*) (\d+);/by (eresolve_tac \1 \2);/;
-s/\bbw\b *([^;]*);/by (rewtac \1);/;
-s/\bbws\b *([^;]*);/by (rewrite_goals_tac \1);/;
-s/\bauto *\(\)/by (Auto_tac())/;
-s/dresolve_tac *\[(\w+)\] */dtac \1 /g;
-s/eresolve_tac *\[(\w+)\] */etac \1 /g;
-s/resolve_tac *\[(\w+)\] */rtac \1 /g;
-s/rewrite_goals_tac *\[(\w+)\]( *)/rewtac \1\2/g;
-s/rtac *\((\w+)\s+RS\s+ssubst\)\s+/stac \1 /g;
--- a/src/Tools/install_html.sh Tue Dec 16 12:17:48 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-#!/bin/csh
-# Executed from the Isabelle src directory, this script transfers all
-# files needed for the HTML version of Isabelle's theories to the HTTP
-# server.
-# If you don't want to copy all the logics, you can supply the names of
-# the wanted ones as parameters as in "install_html.sh HOL HOLCF".
-
-if ( "$*" == "" ) then
- rsh www4 "rm -r .html-data/isabelle/*; mkdir .html-data/isabelle/Tools; \
- chmod og-w .html-data/isabelle/Tools"
-endif
-
-rcp index.html www4:.html-data/isabelle
-rcp Tools/*.gif www4:.html-data/isabelle/Tools
-
-if ( "$*" == "" ) then
- rcp -r CCL CTT Cube FOL FOLP HOL HOLCF LCF Sequents ZF \
- www4:.html-data/isabelle
-else
- rcp -r $* www4:.html-data/isabelle
-endif
-rsh www4 "chgrp -R isabelle .html-data/isabelle/*; chmod -R g+w .html-data/isabelle/*"