lib/Tools/convert
author paulson
Tue, 10 Feb 2004 12:02:11 +0100
changeset 14378 69c4d5997669
parent 11001 6754fa0f2af7
child 14981 e73f8140af78
permissions -rwxr-xr-x
generic of_nat and of_int functions, and generalization of iszero and neg
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     2
#
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     3
# $Id$
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     4
# Author: David von Oheimb, TU Muenchen
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     6
#
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     7
# DESCRIPTION: convert legacy tactic scripts to Isabelle/Isar tactic emulation
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     8
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     9
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    10
## diagnostics
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    11
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    12
PRG="$(basename "$0")"
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    13
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    14
function usage()
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    15
{
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    16
  echo
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    17
  echo "Usage: $PRG [FILES|DIRS...]"
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    18
  echo
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    19
  echo "  Recursively find .ML files, converting legacy tactic scripts to"
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    20
  echo "  Isabelle/Isar tactic emulation."
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    21
  echo "  Note: conversion is only approximated, based on some heuristics."
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    22
  echo
11001
6754fa0f2af7 corrected file name suffixes
oheimb
parents: 10939
diff changeset
    23
  echo "  Renames old versions of FILES by appending \"~0~\"."
6754fa0f2af7 corrected file name suffixes
oheimb
parents: 10939
diff changeset
    24
  echo "  Creates new versions of FILES by appending \".thy\"."
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    25
  echo
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    26
  exit 1
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    27
}
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    28
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    29
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    30
## process command line
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    31
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    32
[ "$#" -eq 0 -o "$1" = "-?" ] && usage
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    33
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    34
SPECS="$@"; shift "$#"
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    35
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    36
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    37
## main
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    38
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    39
#set by configure
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    40
AUTO_PERL=perl
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    41
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    42
find $SPECS \( -name \*.ML \) -print | \
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    43
  xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/convert.pl"