lib/Tools/fixsome
author wenzelm
Wed Nov 22 21:41:39 2000 +0100 (2000-11-22)
changeset 10511 efb3428c9879
parent 9995 8414454c8e11
child 10555 2323ec838401
permissions -rwxr-xr-x
tuned;
wenzelm@9966
     1
#!/bin/bash
wenzelm@9966
     2
#
wenzelm@9966
     3
# $Id$
wenzelm@9966
     4
# Author: Markus Wenzel, TU Muenchen
wenzelm@9966
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@9966
     6
#
wenzelm@9966
     7
# DESCRIPTION: fix theorem names related to SOME (Eps) in HOL
wenzelm@9966
     8
wenzelm@9966
     9
wenzelm@9966
    10
## diagnostics
wenzelm@9966
    11
wenzelm@10511
    12
PRG="$(basename "$0")"
wenzelm@9966
    13
wenzelm@9966
    14
function usage()
wenzelm@9966
    15
{
wenzelm@9966
    16
  echo
wenzelm@9966
    17
  echo "Usage: $PRG [FILES|DIRS...]"
wenzelm@9966
    18
  echo
wenzelm@9995
    19
  echo "  Recursively find .thy/.ML files, fixing theorem names related"
wenzelm@9966
    20
  echo "  to SOME (Eps) in HOL."
wenzelm@9966
    21
  echo
wenzelm@9966
    22
  echo "  Renames old versions of FILES by appending \"~~\"."
wenzelm@9966
    23
  echo
wenzelm@9966
    24
  exit 1
wenzelm@9966
    25
}
wenzelm@9966
    26
wenzelm@9966
    27
wenzelm@9966
    28
## process command line
wenzelm@9966
    29
wenzelm@9966
    30
[ "$#" -eq 0 -o "$1" = "-?" ] && usage
wenzelm@9966
    31
wenzelm@9966
    32
SPECS="$@"; shift "$#"
wenzelm@9966
    33
wenzelm@9966
    34
wenzelm@9966
    35
## main
wenzelm@9966
    36
wenzelm@9966
    37
#set by configure
wenzelm@9966
    38
AUTO_PERL=perl
wenzelm@9966
    39
wenzelm@9995
    40
find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \
wenzelm@9995
    41
  xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixsome.pl"