# HG changeset patch
# User wenzelm
# Date 1122900021 -7200
# Node ID 40759607c5905155ff17722085a2d3aacaa2db3f
# Parent  37e34f315057cada50b2f66ece7b87976cacf35e
obsolete;

diff -r 37e34f315057 -r 40759607c590 lib/Tools/fixclasimp
--- a/lib/Tools/fixclasimp	Mon Aug 01 11:39:33 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# DESCRIPTION: fix references to implicit claset and simpset
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: $PRG [FILES|DIRS...]"
-  echo
-  echo "  Recursively find .ML files, fixing references to"
-  echo "  implicit claset and simpset."
-  echo
-  echo "  Renames old versions of FILES by appending \"~~\"."
-  echo
-  exit 1
-}
-
-
-## process command line
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
-
-SPECS="$@"; shift "$#"
-
-
-## main
-
-#set by configure
-AUTO_PERL=perl
-
-find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixclasimp.pl"
diff -r 37e34f315057 -r 40759607c590 lib/Tools/fixdatatype
--- a/lib/Tools/fixdatatype	Mon Aug 01 11:39:33 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# DESCRIPTION: adapt theories and proof scripts to new datatype package
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: $PRG [FILES|DIRS...]"
-  echo
-  echo "  Recursively find .thy/.ML files, adapting them to"
-  echo "  the new datatype package"
-  echo
-  echo "  Renames old versions of FILES by appending \"~~\"."
-  echo
-  exit 1
-}
-
-
-## process command line
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
-
-SPECS="$@"; shift "$#"
-
-
-## main
-
-#set by configure
-AUTO_PERL=perl
-
-find $SPECS \( -name \*.thy -o -name \*.ML \) -print | \
-  xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixdatatype.pl"
diff -r 37e34f315057 -r 40759607c590 lib/Tools/fixdots
--- a/lib/Tools/fixdots	Mon Aug 01 11:39:33 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# DESCRIPTION: ensure that dots in formulas are followed by non-idents
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: $PRG [FILES|DIRS...]"
-  echo
-  echo "  Recursively find .thy/.ML files, patching them to ensure that"
-  echo "  dots in formulas are followed by non-idents."
-  echo
-  echo "  Renames old versions of FILES by appending \"~~\"."
-  echo
-  exit 1
-}
-
-
-## process command line
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
-
-SPECS="$@"; shift "$#"
-
-
-## main
-
-#set by configure
-AUTO_PERL=perl
-
-find $SPECS \( -name \*.thy -o -name \*.ML \) -print | \
-  xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixdots.pl"
diff -r 37e34f315057 -r 40759607c590 lib/Tools/fixgoal
--- a/lib/Tools/fixgoal	Mon Aug 01 11:39:33 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# DESCRIPTION: replace goal(w) commands by implicit versions Goal(w)
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: $PRG [FILES|DIRS...]"
-  echo
-  echo "  Recursively find .ML files, replacing goal(w)"
-  echo "  commands by implicit versions Goal(w)"
-  echo
-  echo "  Renames old versions of FILES by appending \"~~\"."
-  echo
-  exit 1
-}
-
-
-## process command line
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
-
-SPECS="$@"; shift "$#"
-
-
-## main
-
-#set by configure
-AUTO_PERL=perl
-
-find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixgoal.pl"
diff -r 37e34f315057 -r 40759607c590 lib/Tools/fixseq
--- a/lib/Tools/fixseq	Mon Aug 01 11:39:33 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# DESCRIPTION: fix references to obsolete Pure/Sequence structure
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: $PRG [FILES|DIRS...]"
-  echo
-  echo "  Recursively find .ML files, fixing references to"
-  echo "  the obsolete Pure/Sequence structure."
-  echo
-  echo "  Renames old versions of FILES by appending \"~~\"."
-  echo
-  exit 1
-}
-
-
-## process command line
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
-
-SPECS="$@"; shift "$#"
-
-
-## main
-
-#set by configure
-AUTO_PERL=perl
-
-find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixseq.pl"
diff -r 37e34f315057 -r 40759607c590 lib/scripts/fixclasimp.pl
--- a/lib/scripts/fixclasimp.pl	Mon Aug 01 11:39:33 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# fixclasimp.pl - fix references to implicit claset and simpset
-#
-
-sub fixclasimp {
-    my ($file) = @_;
-
-    open (FILE, $file) || die $!;
-    undef $/; $text = <FILE>; $/ = "\n";         # slurp whole file
-    close FILE || die $!;
-
-    $_ = $text;
-
-    s/set_current_thy\s*"([^"]*)"/context $1.thy/sg;
-
-    s/!\s*simpset/simpset()/sg;
-    s/simpset\s*:=/simpset_ref() :=/sg;
-    s/simpset_of\s*"([^"]*)"/simpset_of $1.thy/sg;
-
-    s/!\s*claset/claset()/sg;
-    s/claset\s*:=/claset_ref() :=/sg;
-    s/claset_of\s*"([^"]*)"/claset_of $1.thy/sg;
-
-
-    $result = $_;
-
-    if ($text ne $result) {
-	print STDERR "fixing $file\n";
-        if (! -f "$file~~") {
-	    rename $file, "$file~~" || die $!;
-        }
-	open (FILE, "> $file") || die $!;
-	print FILE $result;
-	close FILE || die $!;
-    }
-}
-
-
-## main
-
-foreach $file (@ARGV) {
-  eval { &fixclasimp($file); };
-  if ($@) { print STDERR "*** fixclasimp $file: ", $@, "\n"; }
-}
diff -r 37e34f315057 -r 40759607c590 lib/scripts/fixdatatype.pl
--- a/lib/scripts/fixdatatype.pl	Mon Aug 01 11:39:33 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,49 +0,0 @@
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# fixdatatype.pl - adapt theories and proof scripts to new datatype package
-#
-
-sub fixdatatype {
-    my ($file) = @_;
-
-    open (FILE, $file) || die $!;
-    undef $/; $text = <FILE>; $/ = "\n";         # slurp whole file
-    close FILE || die $!;
-
-    $_ = $text;
-
-    ## convert split_type_case[_asm] to type.split[_asm]
-    s/([^"])\bsplit_([\w]+)_case\b/$1$2.split/sg;
-    s/([^"])\bsplit_([\w]+)_case_asm\b/$1$2.split_asm/sg;
-
-    ## delete function name and type after "primrec"
-    s/\bprimrec\b\s+([\w]+|"[^"]+")\s+([\w\.]+)/primrec/sg;
-
-    ## replace specific induct_tac by generic induct_tac
-    s/[\w\.]+\.induct_tac/induct_tac/sg;
-
-    ## replace res_inst_tac ... natE by case_tac
-    s/\bres_inst_tac\b\s*\[\s*\(\s*"[^"]+"\s*,\s*("[^"]+")\s*\)\s*\]\s*natE\b/case_tac $1/sg;
-
-    $result = $_;
-
-    if ($text ne $result) {
-        print STDERR "fixing $file\n";
-        if (! -f "$file~~") {
-            rename $file, "$file~~" || die $!;
-        }
-        open (FILE, "> $file") || die $!;
-        print FILE $result;
-        close FILE || die $!;
-    }
-}
-
-
-## main
-
-foreach $file (@ARGV) {
-  eval { &fixdatatype($file); };
-  if ($@) { print STDERR "*** fixdatatype $file: ", $@, "\n"; }
-}
diff -r 37e34f315057 -r 40759607c590 lib/scripts/fixdots.pl
--- a/lib/scripts/fixdots.pl	Mon Aug 01 11:39:33 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,57 +0,0 @@
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# fixdots.pl - ensure that dots in formulas are followed by non-idents
-#
-# tries to be smart; may produce garbage if nested comments and
-# solitary quotes (") are intermixed badly;
-#
-
-sub fixdots {
-    my ($file) = @_;
-
-    open (FILE, $file) || die $!;
-    undef $/; $text = <FILE>; $/ = "\n";         # slurp whole file
-    close FILE || die $!;
-
-
-    $result = "";
-    $rest = $text;
-
-    while (1) {
-	$_ = $rest;
-	($pre, $str, $rest) =
-	    m/^((?: \(\*.*?\*\) | [^"] )*)      # pre: text or (non-nested!) comments
-            "((?: [^"\\] | \\\S | \\\s+\\ )*)"  # quoted string
-            (.*)$/sx;                           # rest of file
-	if ($str) {
-	    $_ = $str;
-	    if (!m/^[a-zA-Z0-9_\/\.]*$/s && !m/\.ML/s && !m/\.thy/s) {   # exclude filenames!
-		s/([a-zA-Z][a-zA-Z0-9_']*)\.([a-zA-Z])/$1\. $2/sg;
-	    }
-            $result = $result . $pre . '"' . $_ . '"';
-        } else {
- 	    $result = $result . $_;
-    	    last;
-	}
-    }
-
-    if ($text ne $result) {
-	print STDERR "fixing $file\n";
-        if (! -f "$file~~") {
-	    rename $file, "$file~~" || die $!;
-        }
-	open (FILE, "> $file") || die $!;
-	print FILE $result;
-	close FILE || die $!;
-    }
-}
-
-
-## main
-
-foreach $file (@ARGV) {
-  eval { &fixdots($file); };
-  if ($@) { print STDERR "*** fixdots $file: ", $@, "\n"; }
-}
diff -r 37e34f315057 -r 40759607c590 lib/scripts/fixgoal.pl
--- a/lib/scripts/fixgoal.pl	Mon Aug 01 11:39:33 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,44 +0,0 @@
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# fixgoal.pl - replace goal(w) commands by implicit versions Goal(w)
-#
-
-sub fixgoal {
-    my ($file) = @_;
-
-    open (FILE, $file) || die $!;
-    undef $/; $text = <FILE>; $/ = "\n";         # slurp whole file
-    close FILE || die $!;
-
-    ($path, $thy, $ext) = ($file =~ m,^(.*/)?(\w+)(\.\w+)?$,);
-
-    $_ = $text;
-
-    s/^[ \t]*goalw\b\s*\bthy\b/Goalw/mg;
-    s/^[ \t]*goalw\b\s*\b$thy\.thy\b/Goalw/mg;
-    s/^[ \t]*goal\b\s*\bthy\b/Goal/mg;
-    s/^[ \t]*goal\b\s*\b$thy\.thy\b/Goal/mg;
-
-
-    $result = $_;
-
-    if ($text ne $result) {
-	print STDERR "fixing $file\n";
-        if (! -f "$file~~") {
-	    rename $file, "$file~~" || die $!;
-        }
-	open (FILE, "> $file") || die $!;
-	print FILE $result;
-	close FILE || die $!;
-    }
-}
-
-
-## main
-
-foreach $file (@ARGV) {
-  eval { &fixgoal($file); };
-  if ($@) { print STDERR "*** fixgoal $file: ", $@, "\n"; }
-}
diff -r 37e34f315057 -r 40759607c590 lib/scripts/fixseq.pl
--- a/lib/scripts/fixseq.pl	Mon Aug 01 11:39:33 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# fixseq.pl - fix references to obsolete Pure/Sequence structure
-#
-
-sub fixseq {
-    my ($file) = @_;
-
-    open (FILE, $file) || die $!;
-    undef $/; $text = <FILE>; $/ = "\n";         # slurp whole file
-    close FILE || die $!;
-
-    $_ = $text;
-
-
-    s/Sequence\.tl/Seq.tl/sg;
-    s/Sequence\.single/Seq.single/sg;
-    s/Sequence\.seqof/Seq.make/sg;
-    s/Sequence\.seq/Seq.seq/sg;
-    s/Sequence\.s_of_list/Seq.of_list/sg;
-    s/Sequence\.pull/Seq.pull/sg;
-    s/Sequence\.prints/Seq.print/sg;
-    s/Sequence\.null/Seq.empty/sg;
-    s/Sequence\.maps/Seq.map/sg;
-    s/Sequence\.mapp/Seq.mapp/sg;
-    s/Sequence\.list_of_s/Seq.list_of/sg;
-    s/Sequence\.its_right/Seq.it_right/sg;
-    s/Sequence\.interleave/Seq.interleave/sg;
-    s/Sequence\.hd/Seq.hd/sg;
-    s/Sequence\.flats/Seq.flat/sg;
-    s/Sequence\.filters/Seq.filter/sg;
-    s/Sequence\.cons/Seq.cons/sg;
-    s/Sequence\.chop/Seq.chop/sg;
-    s/Sequence\.append/Seq.append/sg;
-
-
-    $result = $_;
-
-    if ($text ne $result) {
-	print STDERR "fixing $file\n";
-        if (! -f "$file~~") {
-	    rename $file, "$file~~" || die $!;
-        }
-	open (FILE, "> $file") || die $!;
-	print FILE $result;
-	close FILE || die $!;
-    }
-}
-
-
-## main
-
-foreach $file (@ARGV) {
-  eval { &fixseq($file); };
-  if ($@) { print STDERR "*** fixseq $file: ", $@, "\n"; }
-}