lib/Tools/fixnumerals

new theory Real/Hyperreal/HyperDef and file fuf.ML

#!/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