# HG changeset patch # User wenzelm # Date 969009453 -7200 # Node ID e2ddb6a124279e1c1b9c1ba21ad84e08e4346ba0 # Parent 1971c8dd09710373f9fff7dfca9b46f7e5717319 fix theorem names related to SOME (Eps) in HOL; diff -r 1971c8dd0971 -r e2ddb6a12427 lib/Tools/fixsome --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/Tools/fixsome Fri Sep 15 11:17:33 2000 +0200 @@ -0,0 +1,40 @@ +#!/bin/bash +# +# $Id$ +# Author: Markus Wenzel, TU Muenchen +# License: GPL (GNU GENERAL PUBLIC LICENSE) +# +# 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 and .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 \*.thy -o -name \*.ML ")" -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixsome.pl" diff -r 1971c8dd0971 -r e2ddb6a12427 lib/scripts/fixsome.pl --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/scripts/fixsome.pl Fri Sep 15 11:17:33 2000 +0200 @@ -0,0 +1,45 @@ +# +# $Id$ +# Author: Markus Wenzel, TU Muenchen +# License: GPL (GNU GENERAL PUBLIC LICENSE) +# +# fixclasimp.pl - fix references to implicit claset and simpset +# + +sub fixclasimp { + my ($file) = @_; + + open (FILE, $file) || die $!; + undef $/; $text = ; $/ = "\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/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 { &fixclasimp($file); }; + if ($@) { print STDERR "*** fixclasimp $file: ", $@, "\n"; } +}