diff -r 98674ac811c4 -r 521065a499c6 src/HOL/ex/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/ex/Mirabelle/lib/scripts/mirabelle.pl	Fri Aug 21 09:44:55 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,114 +0,0 @@
-#
-# Author: Jasmin Blanchette and Sascha Boehme
-#
-# Testing tool for automated proof tools.
-#
-
-use File::Basename;
-
-# environment
-
-my $isabelle_home = $ENV{'ISABELLE_HOME'};
-my $mirabelle_home = $ENV{'MIRABELLE_HOME'};
-my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'};
-my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'};
-my $verbose = $ENV{'MIRABELLE_VERBOSE'};
-my $timeout = $ENV{'MIRABELLE_TIMEOUT'};
-
-my $mirabelle_thy = $mirabelle_home . "/Mirabelle";
-
-
-# arguments
-
-my $actions = $ARGV[0];
-
-my $thy_file = $ARGV[1];
-my $start_line = "0";
-my $end_line = "~1";
-if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) { # FIXME
-  my $thy_file = $1;
-  my $start_line = $2;
-  my $end_line = $3;
-}
-my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy");
-my $new_thy_name = $thy_name . "_Mirabelle";
-my $new_thy_file = $output_path . "/" . $new_thy_name . $ext;
-
-
-# setup
-
-my $setup_thy_name = $thy_name . "_Setup";
-my $setup_file = $output_path . "/" . $setup_thy_name . ".thy";
-my $log_file = $output_path . "/" . $thy_name . ".log";
-
-open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'";
-
-print SETUP_FILE <<END;
-theory "$setup_thy_name"
-imports "$mirabelle_thy"
-begin
-
-setup {* 
-  Mirabelle.set_logfile "$log_file" #>
-  Config.put_thy Mirabelle.timeout $timeout #>
-  Config.put_thy Mirabelle.verbose $verbose #>
-  Config.put_thy Mirabelle.start_line $start_line #>
-  Config.put_thy Mirabelle.end_line $end_line
-*}
-
-END
-
-foreach (split(/:/, $actions)) {
-  if (m/([^[]*)(?:\[(.*)\])?/) {
-    my ($name, $settings_str) = ($1, $2 || "");
-    print SETUP_FILE "setup {* Mirabelle.invoke \"$name\" [";
-    my $sep = "";
-    foreach (split(/,/, $settings_str)) {
-      if (m/\s*(.*)\s*=\s*(.*)\s*/) {
-        print SETUP_FILE "$sep(\"$1\", \"$2\")";
-        $sep = ", ";
-      }
-    }
-    print SETUP_FILE "] *}\n";
-  }
-}
-
-print SETUP_FILE "\nend";
-close SETUP_FILE;
-
-
-# modify target theory file
-
-open(OLD_FILE, "<$thy_file") || die "Cannot open file '$thy_file'";
-my @lines = <OLD_FILE>;
-close(OLD_FILE);
-
-my $thy_text = join("", @lines);
-my $old_len = length($thy_text);
-$thy_text =~ s/\btheory\b[^\n]*\s*\bimports\s/theory $new_thy_name\nimports "$setup_thy_name" /gm;
-die "No 'imports' found" if length($thy_text) == $old_len;
-
-open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'";
-print NEW_FILE $thy_text;
-close(NEW_FILE);
-
-my $root_file = "$output_path/ROOT_$thy_name.ML";
-open(ROOT_FILE, ">$root_file") || die "Cannot create file '$root_file'";
-print ROOT_FILE "use_thy \"$output_path/$new_thy_name\";\n";
-close(ROOT_FILE);
-
-
-# run isabelle
-
-my $r = system "$isabelle_home/bin/isabelle-process " .
-  "-e 'use \"$root_file\";' -q $mirabelle_logic" . "\n";
-
-
-# cleanup
-
-unlink $root_file;
-unlink $new_thy_file;
-unlink $setup_file;
-
-exit $r;
-