# HG changeset patch
# User wenzelm
# Date 882271166 -3600
# Node ID 231730ecaa95f7751c6850b8733defdd55eb0fbf
# Parent  44ff59be6031bc11c72c15143726cc3b1939e7ea
obsolete;

diff -r 44ff59be6031 -r 231730ecaa95 src/Tools/README
--- 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$
diff -r 44ff59be6031 -r 231730ecaa95 src/Tools/expandshort
--- 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;
diff -r 44ff59be6031 -r 231730ecaa95 src/Tools/install_html.sh
--- 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/*"