diff -r 6decc1ffdbed -r 4ab00a2642c3 src/HOL/Mirabelle/lib/Tools/mirabelle
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/lib/Tools/mirabelle	Wed Sep 02 16:23:53 2009 +0200
@@ -0,0 +1,88 @@
+#!/usr/bin/env bash
+#
+# Author: Sascha Boehme
+#
+# DESCRIPTION: testing tool for automated proof tools
+
+
+PRG="$(basename "$0")"
+
+function print_action_names() {
+  TOOLS="$MIRABELLE_HOME/Tools/mirabelle_*.ML"
+  for NAME in $TOOLS
+  do
+    echo $NAME | sed 's/.*mirabelle_\(.*\)\.ML/    \1/'
+  done
+}
+
+function usage() {
+  out="$MIRABELLE_OUTPUT_PATH"
+  timeout="$MIRABELLE_TIMEOUT"
+  echo
+  echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES"
+  echo
+  echo "  Options are:"
+  echo "    -L LOGIC     parent logic to use (default $ISABELLE_LOGIC)"
+  echo "    -T THEORY    parent theory to use (default $MIRABELLE_THEORY)"
+  echo "    -O DIR       output directory for test data (default $out)"
+  echo "    -t TIMEOUT   timeout for each action in seconds (default $timeout)"
+  echo
+  echo "  Apply the given actions (i.e., automated proof tools)"
+  echo "  at all proof steps in the given theory files."
+  echo
+  echo "  ACTIONS is a colon-separated list of actions, where each action is"
+  echo "  either NAME or NAME[KEY=VALUE,...,KEY=VALUE]. Available actions are:"
+  print_action_names
+  echo
+  echo "  FILES is a list of theory files, where each file is either NAME.thy"
+  echo "  or NAME.thy[START:END] and START and END are numbers indicating the"
+  echo "  range the given actions are to be applied."
+  echo
+  exit 1
+}
+
+
+## process command line
+
+# options
+
+while getopts "L:T:O:t:?" OPT
+do
+  case "$OPT" in
+    L)
+      MIRABELLE_LOGIC="$OPTARG"
+      ;;
+    T)
+      MIRABELLE_THEORY="$OPTARG"
+      ;;
+    O)
+      MIRABELLE_OUTPUT_PATH="$OPTARG"
+      ;;
+    t)
+      MIRABELLE_TIMEOUT="$OPTARG"
+      ;;
+    \?)
+      usage
+      ;;
+  esac
+done
+
+shift $(($OPTIND - 1))
+
+ACTIONS="$1"
+
+shift
+
+
+# setup
+
+mkdir -p "$MIRABELLE_OUTPUT_PATH"
+
+
+## main
+
+for FILE in "$@"
+do
+  perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$ACTIONS" "$FILE"
+done
+