these hacks are no longer needed
authorpaulson
Tue, 17 Jan 2006 10:26:50 +0100
changeset 18701 98e6a0a011f3
parent 18700 f04a8755d6ca
child 18702 7dc7dcd63224
these hacks are no longer needed
src/HOL/Tools/ATP/remchars.pl
src/HOL/Tools/ATP/spassshell
src/HOL/Tools/ATP/testoutput.py
--- 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";
--- 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
-
--- 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()
-