# HG changeset patch
# User wenzelm
# Date 875538982 -7200
# Node ID fec0f996ae67d2523cd8b4670fdcdd69b48d4ecb
# Parent  6fccb16a7e3a8da594007a57a7e10b42f5e6bb7d
superficial;

diff -r 6fccb16a7e3a -r fec0f996ae67 src/Tools/Makefile
--- a/src/Tools/Makefile	Mon Sep 29 15:11:27 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-OPTIONS= -DDEBUG
-CC = g++ $(OPTIONS)
-OBJS = qed.o
-
-.SUFFIXES: .cc .o
-
-.cc.o:
-	$(CC) -c $<
-
-qed:	$(OBJS)
-	g++ -o qed $(OBJS)
diff -r 6fccb16a7e3a -r fec0f996ae67 src/Tools/qed.cc
--- a/src/Tools/qed.cc	Mon Sep 29 15:11:27 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,163 +0,0 @@
-// Little utility to convert result() -> qed ... in Isabelle's files
-// Written in 1995 by Carsten Clasohm (clasohm@informatik.tu-muenchen.de)
-
-#define LIN_LEN   1000		// maximal length of lines in sourcefile
-
-#include <iostream.h>
-#include <fstream.h>
-#include <string.h>
-#include <assert.h>
-#include <stdio.h>
-#include <unistd.h>
-#include <ctype.h>
-
-// Null terminated list of theorem names that must not be included in the
-// theorem database
-char * excludeName[] = {"temp", "tmp", 0};
-
-int ExcludeThm(char *name)
-{
-    for (int i = 0; excludeName[i]; i++)
-	if (strcmp(name, excludeName[i]) == 0)
-	    return 1;
-    return 0;
-}
-
-main(int argc, char *argv[])
-{
-    char l[LIN_LEN];
-    int lines = 0;
-
-    // Open input and output files
-    ifstream in(argv[1]);
-    ofstream out(argv[2]);
-
-    if (in.bad() || out.bad())
-    {
-        cerr << "qed version 1.00, Written in 1994 by Carsten Clasohm"
-                "(clasohm@informatik.tu-muenchen.de)\n\n";
-	cerr << "Usage: qed <infile> <outfile>\n";
-	exit(1);
-    }
-
-#ifdef DEBUG
-    cerr << "Processing file " << argv[1] << '\n';
-#endif
-
-    // Process each line separatly
-    in.getline(l, LIN_LEN);
-    while (!in.eof())
-    {
-	char *rPos;
-	char *valPos;
-	char *eqPos;
-	char *tmp;
-
-	if ((rPos = strstr(l, "result()")) && (!isalnum(*(rPos-1)))
-	    && (valPos = strstr(l, "val ")) && (eqPos = strstr(l, "=")))
-	{                            // does line contain "result()" and "val"?
-	    char name[LIN_LEN];
-
-	    assert(eqPos-(valPos+4) > 0);
-	    strncpy(name, valPos+4, eqPos-(valPos+4));
-	    name[eqPos-(valPos+4)] = 0;
-	    if (!isalnum(name[eqPos-(valPos+4)-1]))
-	        name[eqPos-(valPos+4)-1] = 0;
-#ifdef DEBUG
-	    cerr << "Found result: \"" << name << "\"\n";
-#endif
-	    char prefix[LIN_LEN];
-	    char arg[LIN_LEN];
-
-	    if (ExcludeThm(name))
-		out << l << '\n';
-	    else if ((rPos - eqPos < 5) && (rPos == strstr(l, "result();")))
-	    {                                              // replace by "qed"?
-		strncpy(prefix, l, valPos-l);
-		prefix[valPos-l] = 0;
-		out << prefix << "qed \"" << name << "\";" << '\n';
-	    }
-	    else				         // replace by bind_thm
-	    {                                           
-		int d = (*(eqPos+1) == ' ') ? 2 : 1;
-		strcpy(arg, eqPos+d);
-		arg[strlen(arg)-1] = 0;
-		strcpy(prefix, l);
-		prefix[valPos-l] = 0;
-		out << prefix << "bind_thm(\"" << name << "\", "
-		    << arg << ");\n";
-	    }
-	}
-	else if ((rPos = strstr(l, "prove_goal")) 
-		 && (!isalnum(*(rPos-1))) 
-		 && (!isalnum(*(rPos+10)) || (*(rPos+10) == 'w'))
-		 && (valPos = strstr(l, "val ")) 
-		 && (eqPos = strstr(l, "="))
-                 && (rPos - eqPos < 5))
-	{                                    // replace prove_goal by qed_goal?
-	    char name[LIN_LEN];
-
-	    assert(eqPos-(valPos+4) > 0);
-	    strncpy(name, valPos+4, eqPos-(valPos+4));
-	    name[eqPos-(valPos+4)] = 0;
-	    if (!isalnum(name[eqPos-(valPos+4)-1]))
-	        name[eqPos-(valPos+4)-1] = 0;
-#ifdef DEBUG
-	    cerr << "Found prove_goal: \"" << name << "\"\n";
-#endif
-	    if (ExcludeThm(name))
-		out << l << '\n';
-	    else
-	    {
-	        char prefix[LIN_LEN];
-	        char arg[LIN_LEN];
-
-	        strncpy(prefix, l, valPos-l);
-	        prefix[valPos-l] = 0;
-	        out << prefix << "qed_goal"
-                    << ((*(rPos+10) == 'w') ? "w " : " ")
-		    << '\"' << name << '\"' << strchr(rPos, ' ') << '\n';
-	    }
-	}
-	else if ((rPos = strstr(l, "standard"))
-		 && (!isalnum(*(rPos-1))) 
-		 && (!isalnum(*(rPos+8))) 
-		 && (valPos = strstr(l, "val ")) 
-		 && (eqPos = strstr(l, "="))
-                 && (rPos - eqPos < 5)
-                 && (l[strlen(l)-1] == ';'))
-	{                                                   // insert bind_thm?
-	    char name[LIN_LEN];
-
-	    assert(eqPos-(valPos+4) > 0);
-	    strncpy(name, valPos+4, eqPos-(valPos+4));
-	    name[eqPos-(valPos+4)] = 0;
-	    if (!isalnum(name[eqPos-(valPos+4)-1]))
-	        name[eqPos-(valPos+4)-1] = 0;
-#ifdef DEBUG
-	    cerr << "Found standard: \"" << name << "\"\n";
-#endif
-	    if (ExcludeThm(name))
-		out << l << '\n';
-	    else
-	    {
-	        char prefix[LIN_LEN];
-	        char arg[LIN_LEN];
-
-	        strncpy(prefix, l, valPos-l);
-	        prefix[valPos-l] = 0;
-	        strcpy(l+strlen(l)-1, ");");    // insert ")" before line's ';'
-	        out << prefix << "bind_thm (\"" << name << "\","
-	            << strchr(rPos, ' ') << '\n';
-            }
-	}
-	else                                           // output line unchanged
-	    out << l << '\n';
-	in.getline(l, LIN_LEN);
-    }
-    in.close();
-    out.close();
-#ifdef DEBUG
-    cerr << "Done\n";
-#endif
-}
diff -r 6fccb16a7e3a -r fec0f996ae67 src/Tools/qed.doc
--- a/src/Tools/qed.doc	Mon Sep 29 15:11:27 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,97 +0,0 @@
-			Documentation for qed
-
-qed is a utility that's able to (almost) automatically insert calls to
-Isabelle's functions qed, qed_goal, qed_goalw and bind_thm into ML
-files.  It does this by looking for certain patterns and changing the
-line so that the theorems are added to Isabelle's theorem database.
-The intent of including it into the distribution is to enable you to
-convert existing theory files.
-
-
-Compilation
------------
-
-qed was written in C++ and compiled using g++ 2.5.8. Executing "make qed"
-should create the executable.
-
-
-Usage
------
-
-To start qed type:
-
-qed <infile> <outfile>
-
-<infile> is the ML file you want to convert and <outfile> is the file
-to which the output should be sent. If you want to convert a whole
-directory of ML files and keep the original files as <name>.bak you
-can use the script 'runqed'.
-
-During its execution qed will output the names of all theorems that it has
-found.
-
-
-Recognized Theorems
--------------------
-
-Because qed knows nothing about ML's syntax it has to rely on certain
-assumptions about how typical definitions of theorems look. These
-assumptions were made based on the files contained in the distribution
-and therefore it's possible that they do not fit for the files you
-want to convert. So if qed does not do what you expect it to do have a
-look at the following list.
-
-
--    val mono_Int = result();
-  -> qed "mono_Int";
-
-  This kind of line is recognized if it contains "val ", "=" and the word
-  "result();" and if the distance between "=" and "result()" is less
-  than 5 characters.
-
-
--    val XHlemma2 = result() RS mp;
-  -> bind_thm("XHlemma2", result() RS mp);
-
-  If the first case cannot be applied because the "=" and "result()" are too
-  far apart or "result()" is not followed by a ";" this one is
-  used.
-
-  
--    val sym = prove_goal HOL.thy "s=t ==> t=s"
-  -> qed_goal "sym" HOL.thy "s=t ==> t=s"
-
-  Lines containing the word "prove_goal" or "prove_goalw" and the strings
-  "val " and "=" with a distance between "prove_goal" and "=" of less
-  than 5 characters are matched by this case. Note that the ML command
-  continues in the next line but is not changed further.
-
-
--    val ssubst = standard (sym RS subst);
-  -> bind_thm ("ssubst", (sym RS subst));
-
-  A line in which the word "standard" and the strings "val " and "=" can be
-  found (with the usual distance limitation) and which ends with ";" is
-  converted this way.
-
-
-At least for the standard theories these rules only match the desired
-kind of lines. It is possible though that not all places for insertion
-of the theorem database functions are found. Also qed has no way to
-recognize ML commands such as "local ... in ... end" or "let ... in
-... end". Processing files where theorems are defined inside these
-commands leads to syntax errors during compilation of the generated
-files like e.g. "end expected but bind_thm was found". One can avoid
-this by changing the affected lines to "val _ = bind_thm ..." after the
-conversion or by manually editing the original file.
-
-
-Problems?
---------
-
-If qed does not do what you want it to do you could change the
-sourcecode (qed.cc) yourself which should be fairly easy.  If qed does
-not handle a case that you regard as a 'typical' way of defining a
-theorem (i.e. one that occurs very often in your files) send an email
-containg some examples to clasohm@informatik.tu-muenchen.de.
-
diff -r 6fccb16a7e3a -r fec0f996ae67 src/Tools/runqed
--- a/src/Tools/runqed	Mon Sep 29 15:11:27 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-#! /bin/csh
-# $Id$
-# Run qed on all ML files in the current directory
-foreach f (*ML)
-echo Expanding shorthands in $f. \ Backup file is $f:r.bak
-qed $f $f:r.MLL
-mv $f $f:r.bak
-mv $f:r.MLL $f
-end
-echo Finished.