diff -r 56c96c02ab79 -r 9a786d5f8821 lib/Tools/convert --- a/lib/Tools/convert Sat Jun 14 17:26:14 2008 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,39 +0,0 @@ -#!/usr/bin/env bash -# -# $Id$ -# Author: David von Oheimb, TU Muenchen -# -# DESCRIPTION: convert legacy tactic scripts to Isabelle/Isar tactic emulation - - -## diagnostics - -PRG="$(basename "$0")" - -function usage() -{ - echo - echo "Usage: $PRG [FILES|DIRS...]" - echo - echo " Recursively find .ML files, converting legacy tactic scripts to" - echo " Isabelle/Isar tactic emulation." - echo " Note: conversion is only approximated, based on some heuristics." - echo - echo " Renames old versions of FILES by appending \"~0~\"." - echo " Creates new versions of FILES by appending \".thy\"." - echo - exit 1 -} - - -## process command line - -[ "$#" -eq 0 -o "$1" = "-?" ] && usage - -SPECS="$@"; shift "$#" - - -## main - -find $SPECS \( -name \*.ML \) -print | \ - xargs perl -w "$ISABELLE_HOME/lib/scripts/convert.pl"