# HG changeset patch
# User wenzelm
# Date 1207662435 -7200
# Node ID 13bbc72fda45986736554feec596d70998a689fe
# Parent  e6511a920168c0ceb1ecc4dbbab89daa556e9a12
obsolete;

diff -r e6511a920168 -r 13bbc72fda45 lib/Tools/expandshort
--- a/lib/Tools/expandshort	Tue Apr 08 15:47:14 2008 +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: expand shorthand goal commands
-
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: $PRG [FILES|DIRS...]"
-  echo
-  echo "  Recursively find .ML files, expand shorthand goal commands.  Also"
-  echo "  contracts uses of resolve_tac, dresolve_tac, eresolve_tac,"
-  echo "  forward_tac, rewrite_goals_tac on 1-element lists; furthermore"
-  echo "  expands tabs, which are forbidden in SML string constants."
-  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/expandshort.pl"
diff -r e6511a920168 -r 13bbc72fda45 lib/Tools/fixcpure
--- a/lib/Tools/fixcpure	Tue Apr 08 15:47:14 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Makarius
-#
-# DESCRIPTION: adapt theories and ML files to new CPure/Pure arrangement
-
-
-## 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 CPure/Pure arrangement"
-  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/fixcpure.pl"
diff -r e6511a920168 -r 13bbc72fda45 lib/Tools/fixgreek
--- a/lib/Tools/fixgreek	Tue Apr 08 15:47:14 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Sebastian Skalberg, TU Muenchen
-#
-# DESCRIPTION: fix problems with greek and other foreign letters
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: $PRG [FILES|DIRS...]"
-  echo
-  echo "  Recursively find .thy files, fixing parse problems stemming"
-  echo "  from the classification change of greek and other foreign"
-  echo "  letters from symbols to letters."
-  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 -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixgreek.pl"
-find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixgreek.pl"
diff -r e6511a920168 -r 13bbc72fda45 lib/Tools/fixsome
--- a/lib/Tools/fixsome	Tue Apr 08 15:47:14 2008 +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: fix theorem names related to SOME (Eps) in HOL
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: $PRG [FILES|DIRS...]"
-  echo
-  echo "  Recursively find .thy/.ML files, fixing theorem names related"
-  echo "  to SOME (Eps) in HOL."
-  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 -o -name \*.thy \) -print | \
-  xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixsome.pl"
diff -r e6511a920168 -r 13bbc72fda45 lib/scripts/configure
--- a/lib/scripts/configure	Tue Apr 08 15:47:14 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-#!/bin/sh
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# configure - adapt Isabelle distribution to system environment
-
-## patch scripts
-
-cd "`dirname "$0"`"
-
-if bash -c :
-then
-  bash lib/scripts/patch-scripts.bash
-else
-  echo "FATAL ERROR: bash not found!"
-  exit 2
-fi
diff -r e6511a920168 -r 13bbc72fda45 lib/scripts/expandshort.pl
--- a/lib/scripts/expandshort.pl	Tue Apr 08 15:47:14 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,61 +0,0 @@
-#
-# $Id$
-#
-# expandshort.pl - expand shorthand goal commands
-#
-# in "be ... i;" -> "by (etac ... i);" the "..." phrase is not allowed to
-#   contain punctuation.  Otherwise, comments can be affected!
-# a special case is made to detect    be alpha.alpha digits   
-#
-
-sub expandshort {
-    my ($file) = @_;
-
-    open (FILE, $file) || die $!;
-    undef $/; $text = <FILE>; $/ = "\n";         # slurp whole file
-    close FILE || die $!;
-
-    $_ = $text;
-
-    s/\bsafe_tac *\(claset *\( *\) *\)/Safe_tac/sg;
-    s/ *\(Safe_tac\) *([0-9]+)/ Safe_tac $1/sg;
-    s/ *\(Safe_tac\)/ Safe_tac/sg;
-    s/\bby\(/by (/sg;
-    s/\bba\b *(\d+);/by (assume_tac $1);/sg;
-    s/\bbr\b *([^;*!]*) (\d+);/by (rtac $1 $2);/sg;
-    s/\bbrs\b *([^;*!]*) (\d+);/by (resolve_tac $1 $2);/sg;
-    s/\bbd\b *([^;*!]*) (\d+);/by (dtac $1 $2);/sg;
-    s/\bbds\b *([^;*!]*) (\d+);/by (dresolve_tac $1 $2);/sg;
-    s/\bbe\b *([^;.*!]*) (\d+);/by (etac $1 $2);/sg;
-    s/\bbe\b *(\w+\.\w+) (\d+);/by (etac $1 $2);/sg;
-    s/\bbes\b *([^;*!]*) (\d+);/by (eresolve_tac $1 $2);/sg;
-    s/\bbw\b *([^;*!]*);/by (rewtac $1);/sg;
-    s/\bbws\b *([^;*!]*);/by (rewrite_goals_tac $1);/sg;
-    s/\bauto *\(\)/by Auto_tac/sg;
-    s/dresolve_tac *\[(\w+)\] */dtac $1 /sg;
-    s/eresolve_tac *\[(\w+)\] */etac $1 /sg;
-    s/forward_tac *\[(\w+)\] */ftac $1 /sg;
-    s/resolve_tac *\[(\w+)\] */rtac $1 /sg;
-    s/rewrite_goals_tac *\[(\w+)\]( *)/rewtac $1$2/sg;
-    s/rtac *\((\w+)\s+RS\s+ssubst\)\s+/stac $1 /sg;
-
-    $result = $_;
-
-    if ($text ne $result) {
-	print STDERR "expanding $file\n";
-        if (! -f "$file~~") {
-	    rename $file, "$file~~" || die $!;
-        }
-	open (FILE, "> $file") || die $!;
-	print FILE $result;
-	close FILE || die $!;
-    }
-}
-
-
-## main
-
-foreach $file (@ARGV) {
-  eval { &expandshort($file); };
-  if ($@) { print STDERR "*** expandshort $file: ", $@, "\n"; }
-}
diff -r e6511a920168 -r 13bbc72fda45 lib/scripts/fixcpure.pl
--- a/lib/scripts/fixcpure.pl	Tue Apr 08 15:47:14 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-#
-# $Id$
-# Author: Makarius
-#
-# fixcpure.pl - adapt theories and ML files to new CPure/Pure arrangement
-#
-
-sub fixcpure {
-    my ($file) = @_;
-
-    open (FILE, $file) || die $!;
-    undef $/; $text = <FILE>; $/ = "\n";         # slurp whole file
-    close FILE || die $!;
-
-    $_ = $text;
-
-    s/\bCPure\.thy\b/-THE-CPURE-THEORY-/sg;
-    s/\bCPure\.([A-Za-z_\-])/Pure.$1/sg;
-    s/-THE-CPURE-THEORY-/CPure.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 { &fixcpure($file); };
-  if ($@) { print STDERR "*** fixcpure $file: ", $@, "\n"; }
-}
diff -r e6511a920168 -r 13bbc72fda45 lib/scripts/fixgreek.pl
--- a/lib/scripts/fixgreek.pl	Tue Apr 08 15:47:14 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,49 +0,0 @@
-#
-# $Id$
-# Author: Sebastian Skalberg, TU Muenchen
-#
-# fixgreek.pl - fix problems with greek and other foreign letters now
-#               being classified as letters instead of symbols.
-#
-
-sub fixgreek {
-    my ($file) = @_;
-
-    open (FILE, $file) || die $!;
-    undef $/; $text = <FILE>; $/ = "\n";         # slurp whole file
-    close FILE || die $!;
-
-    $_ = $text;
-
-    s/(\\<(a|b|c|d|e|f|g|h|i|j|k|l|m|n|o|p|q|r|s|t|u|v|w|x|y|z|A|B|C|D|E|F|G|H|I|J|K|L|M|N|O|P|Q|R|S|T|U|V|W|X|Y|Z)>)([a-zA-Z0-9])/$1 $3/sg;
-
-    s/([a-zA-Z][a-zA-Z0-9]*)(\\<(a|b|c|d|e|f|g|h|i|j|k|l|m|n|o|p|q|r|s|t|u|v|w|x|y|z|A|B|C|D|E|F|G|H|I|J|K|L|M|N|O|P|Q|R|S|T|U|V|W|X|Y|Z)>)/$1 $2/sg;
-
-    s/(\\<(aa|bb|cc|dd|ee|ff|gg|hh|ii|jj|kk|ll|mm|nn|oo|pp|qq|rr|ss|tt|uu|vv|ww|xx|yy|zz|AA|BB|CC|DD|EE|FF|GG|HH|II|JJ|KK|LL|MM|NN|OO|PP|QQ|RR|SS|TT|UU|VV|WW|XX|YY|ZZ)>)([a-zA-Z0-9])/$1 $3/sg;
-
-    s/([a-zA-Z][a-zA-Z0-9]*)(\\<(aa|bb|cc|dd|ee|ff|gg|hh|ii|jj|kk|ll|mm|nn|oo|pp|qq|rr|ss|tt|uu|vv|ww|xx|yy|zz|AA|BB|CC|DD|EE|FF|GG|HH|II|JJ|KK|LL|MM|NN|OO|PP|QQ|RR|SS|TT|UU|VV|WW|XX|YY|ZZ)>)/$1 $2/sg;
-
-    s/(\\<(alpha|beta|gamma|delta|epsilon|zeta|eta|theta|iota|kappa|mu|nu|xi|pi|rho|sigma|tau|upsilon|phi|psi|omega|Gamma|Delta|Theta|Lambda|Xi|Pi|Sigma|Upsilon|Phi|Psi|Omega)>)([a-zA-Z0-9])/$1 $3/sg;
-
-    s/([a-zA-Z][a-zA-Z0-9]*)(\\<(alpha|beta|gamma|delta|epsilon|zeta|eta|theta|iota|kappa|mu|nu|xi|pi|rho|sigma|tau|upsilon|phi|psi|omega|Gamma|Delta|Theta|Lambda|Xi|Pi|Sigma|Upsilon|Phi|Psi|Omega)>)/$1 $2/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 { &fixgreek($file); };
-  if ($@) { print STDERR "*** fixgreek $file: ", $@, "\n"; }
-}
diff -r e6511a920168 -r 13bbc72fda45 lib/scripts/fixsome.pl
--- a/lib/scripts/fixsome.pl	Tue Apr 08 15:47:14 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# fixsome.pl - fix theorem names related to SOME (Eps) in HOL
-#
-
-sub fixsome {
-    my ($file) = @_;
-
-    open (FILE, $file) || die $!;
-    undef $/; $text = <FILE>; $/ = "\n";         # slurp whole file
-    close FILE || die $!;
-
-    $_ = $text;
-
-    s/select_equality/some_equality/g;
-    s/select_eq_Ex/some_eq_ex/g;
-    s/selectI2EX/someI2_ex/g;
-    s/selectI2/someI2/g;
-    s/selectI/someI/g;
-    s/select1_equality/some1_equality/g;
-    s/Eps_sym_eq/some_sym_eq_trivial/g;
-    s/Eps_eq/some_eq_trivial/g;
-
-    $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 { &fixsome($file); };
-  if ($@) { print STDERR "*** fixsome $file: ", $@, "\n"; }
-}
diff -r e6511a920168 -r 13bbc72fda45 lib/scripts/patch-scripts.bash
--- a/lib/scripts/patch-scripts.bash	Tue Apr 08 15:47:14 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,52 +0,0 @@
-# -*- shell-script -*-
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# patch-scripts.bash - relocate interpreter paths of executable scripts and
-#   insert AUTO_BASH/AUTO_PERL values
-#
-
-## find binaries
-
-function findbin()
-{
-  local BASE="$1"
-  local BINARY=""
-
-  BINARY=$(type -path "$BASE")
-
-  if [ -n "$BINARY" ]; then
-    echo "found $BINARY" >&2
-    echo "$BINARY"
-    return
-  else
-    echo "ERROR: $BASE not found!" >&2
-    echo "$DEFAULT"
-    return
-  fi
-}
-
-
-## main
-
-[ -z "$BASH_PATH" ] && BASH_PATH=$(findbin bash)
-[ -z "$PERL_PATH" ] && PERL_PATH=$(findbin perl)
-[ -z "$AUTO_BASH" ] && AUTO_BASH="$BASH_PATH"
-[ -z "$AUTO_PERL" ] && AUTO_PERL="$PERL_PATH"
-
-for FILE in $(find . -type f -print)
-do
-  if [ -x "$FILE" ]; then
-    sed -e "s:^#!.*/bash:#!$BASH_PATH:" -e "s:^#!.*/perl:#!$PERL_PATH:" \
-      -e "s:^AUTO_BASH=.*bash:AUTO_BASH=$AUTO_BASH:" \
-      -e "s:^AUTO_PERL=.*perl:AUTO_PERL=$AUTO_PERL:" "$FILE" > "$FILE~~"
-    if cmp -s "$FILE" "$FILE~~"; then
-      rm "$FILE~~"
-    else
-      rm -f "$FILE"
-      mv "$FILE~~" "$FILE"
-      chmod +x "$FILE"
-      echo "fixed $FILE"
-    fi
-  fi
-done