diff -r b053e0ab9f60 -r aa1d0d620031 lib/Tools/fixnumerals
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/fixnumerals	Fri Jul 23 14:05:50 1999 +0200
@@ -0,0 +1,63 @@
+#!/bin/bash
+#
+# $Id$
+#
+# DESCRIPTION: fix occurences of numerals in HOL/ZF terms
+
+
+## diagnostics
+
+PRG=$(basename $0)
+
+function usage()
+{
+  echo
+  echo "Usage: $PRG [FILES|DIRS...]"
+  echo
+  echo "  Options are:"
+  echo "    -c           add '(_::int)' type constraints (for HOL only)"
+  echo
+  echo "  Recursively find .thy/.ML files, fixing occurences of"
+  echo "  HOL/ZF numerals: #42 becomes 42, #-42 becomes ~42".
+  echo
+  echo "  Renames old versions of FILES by appending \"~~\"."
+  echo
+  exit 1
+}
+
+
+## process command line
+
+# options
+
+CONSTRAINTS=false
+
+while getopts "c" OPT
+do
+  case "$OPT" in
+    c)
+      CONSTRAINTS=true
+      ;;
+    \?)
+      usage
+      ;;
+  esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+[ $# -eq 0 ] && 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/fixnumerals.pl $CONSTRAINTS