# HG changeset patch
# User paulson
# Date 1137490010 -3600
# Node ID 98e6a0a011f36ec4250aa199c45be2cf6ad5f8b8
# Parent  f04a8755d6ca7235d7d05bc6309e87a02be12617
these hacks are no longer needed

diff -r f04a8755d6ca -r 98e6a0a011f3 src/HOL/Tools/ATP/remchars.pl
--- a/src/HOL/Tools/ATP/remchars.pl	Tue Jan 17 10:26:36 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-#!/usr/bin/perl
-#
-# isa2tex.pl - Converts isabelle formulae into LaTeX
-# A complete hack - needs more work.
-#
-# by Michael Dales (michael@dcs.gla.ac.uk)
-
-# Begin math mode
-#printf "\$";
-#ALL íxaè::ê'aè::étypeè.   (~ (ìPè::ê'aè::étypeè => bool) (ìxè::ê'aè::étypeè) | ìPè íxaè) & (~ ìPè íxaè# | ìPè ìxè)((ìPè::ê'aè::étypeè => bool) (ìxaè::ê'aè::étypeè) | (ALL íxè::ê'aè::étypeè. ìPè íxè)) &((AL#L íxè::ê'aè::étypeè. ~ ìPè íxè) | ~ ìPè (ìxbè::ê'aè::étypeè))
-#perhaps change to all chars not in alphanumeric or a few symbols?
-
-while (<STDIN>)
-{
-
-    #chop();
-    s%\n$%%;
-    s%í%%g;
-    s%ì%%g;
-    s%è%%g;
-    s%î%%g;
-    s%ê%%g;
-    s%é%%g;
-    
-    #printf "$_\\newline\n";
-    printf "$_";
-}
-
-# End math mode
-#printf "\$\n";
-#printf "\\end{tabbing}\n";
diff -r f04a8755d6ca -r 98e6a0a011f3 src/HOL/Tools/ATP/spassshell
--- a/src/HOL/Tools/ATP/spassshell	Tue Jan 17 10:26:36 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-#!/bin/sh
-#  ID: $Id$
-# Shell script to invoke SPASS and filter the output
-
-`isatool getenv -b SPASS_HOME`/SPASS  $* | \
-    `isatool getenv -b ISABELLE_HOME`/src/HOL/Tools/ATP/testoutput.py
-
diff -r f04a8755d6ca -r 98e6a0a011f3 src/HOL/Tools/ATP/testoutput.py
--- a/src/HOL/Tools/ATP/testoutput.py	Tue Jan 17 10:26:36 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-#!/usr/bin/python
-
-import string
-import sys
-
-mode = 0
-try:
-  while 1:
-    line = sys.stdin.readline()
-    words = line.split()
-    if len(words) > 0:
-      if words[0] == "SPASS":
-        mode = 1
-    if line == '':
-      break
-    line = line[:-1]
-    if mode == 1:
-      print line
-except:
-  pass
-#f.close()
-
-sys.exit()
-