1.1 --- a/src/Tools/agrep	Tue Sep 30 16:12:38 1997 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,3 +0,0 @@
     1.4 -#! /bin/csh
     1.5 -grep "$*" */*.ML */*/*.ML TFL/*.sml TFL/*.sig TFL/examples/Subst/*.ML
     1.6 -

     2.1 --- a/src/Tools/change_simp	Tue Sep 30 16:12:38 1997 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,21 +0,0 @@
     2.4 -#! /bin/sh
     2.5 -# $Id$
     2.6 -#Assists in converting uses of the old simplifier (Isabelle-92 and earlier)
     2.7 -#Usage:
     2.8 -#    change_simp FILE1 ... FILEn
     2.9 -#
    2.10 -#Renames old versions of the files as FILE1~~ ... FILEn~~
    2.11 -#
    2.12 -for f in $*
    2.13 -do
    2.14 -echo $f. \ Backup file is $f~~
    2.15 -mv $f $f~~; sed -e '
    2.16 -s/\<ASM_SIMP_TAC\>/asm_simp_tac/g
    2.17 -s/\<SIMP_TAC\>/simp_tac/g
    2.18 -s/\<addrews\>/addsimps/g
    2.19 -s/addsplits \(\[[^]]*\]\)/setloop (split_tac \1)/g
    2.20 -s/addsplits/setloop  split_tac/g
    2.21 -s/\<setauto\>/setsolver/g
    2.22 -' $f~~ > $f
    2.23 -done
    2.24 -echo Finished.

     3.1 --- a/src/Tools/conv-theory-files.pl	Tue Sep 30 16:12:38 1997 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,53 +0,0 @@
     3.4 -#!/usr/bin/perl -s-	 # -*-Perl-*-
     3.5 -
     3.6 -#---------------------------------------------------------------------
     3.7 -#The following script file is useful to convert old theory files into a
     3.8 -#style consistent with new naming conventions. Now, the names of the
     3.9 -#files must be the same as the names of the theories they define (with
    3.10 -#a ".thy" suffix) and corresponding ML files must also be renamed.
    3.11 -#
    3.12 -#To make this renaming easier, the following perl script can be used.
    3.13 -#It traverses the given directory recursively.  For each file of the
    3.14 -#form abc.thy, this script does the following steps:
    3.15 -#
    3.16 -#1. Reads the file and grabs the first identifier, say Abc (skipping comments
    3.17 -#   (*...*) and white space).
    3.18 -#2. Outputs the commands needed to rename the file abc.thy to Abc.thy,
    3.19 -#   including the appropriate CVS commands.
    3.20 -#3. If abc.ML also exists, it outputs appropriate commands to rename it
    3.21 -#   to Abc.ML.
    3.22 -#
    3.23 -#These commands can be put into a file, which can then be executed.
    3.24 -#If you are not using cvs, use "grep" to extract just the "mv" commands.
    3.25 -#
    3.26 -#						- Sara Kalvala
    3.27 -#						  (sk@cl.cam.ac.uk)
    3.28 -#---------------------------------------------------------------------
    3.29 -
    3.30 -open(MATCH_FILES, "find . -name \"*thy\" -print |");
    3.31 -
    3.32 -foreach $each_match (<MATCH_FILES>) {
    3.33 - chop($each_match);
    3.34 - if($each_match =~ /(.*\/)(\w*)\.thy/) {$dirpart = $1;}
    3.35 - else {print "something wrong with finding path!\n";
    3.36 -       $dirpart = "";}
    3.37 - open (CONTENTS, $each_match);
    3.38 - @readit = <CONTENTS>;
    3.39 - chop(@readit); $oneline = join(" ",@readit);
    3.40 - $oneline =~ s/\(\*([^\*]|(\*[^\)]))*\*\)//g ;
    3.41 -# comments: have to remove strings of anything but stars or stars
    3.42 -# followed by anything but right parenthesis 
    3.43 - if($oneline =~ /\s*([^ ]*)\s*=.*/)
    3.44 - {$th_name = $1;
    3.45 -  $new_name = $dirpart . $th_name . ".thy";
    3.46 -  print "mv -i $each_match $new_name \n";
    3.47 -  print "cvs rm $each_match ; cvs add $new_name \n";
    3.48 -# for ML files
    3.49 -  $each_ML = $each_match;
    3.50 -  $each_ML =~ s/.thy/.ML/;
    3.51 -  if (-e $each_ML) { $new_ML = $dirpart . $th_name . ".ML";
    3.52 -		     print "mv -i $each_ML $new_ML \n";
    3.53 -		     print "cvs rm $each_ML ; cvs add $new_ML \n";}}
    3.54 - else {print "something wrong with format of theory file!\n";}
    3.55 -}
    3.56 -