# HG changeset patch
# User wenzelm
# Date 870859199 -7200
# Node ID 1e7621573d9ca4735efdd688002cea1bd7187482
# Parent  b689656214eafba0a4724ce1d0d2891c0e6412a4
obsolete!

diff -r b689656214ea -r 1e7621573d9c src/HOLCF/ax_ops/install.tex
--- a/src/HOLCF/ax_ops/install.tex	Wed Aug 06 01:18:31 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-
-Um diese Erweiterung zu installieren, gen\"ugt es nat\"urlich nicht, die
-Sourcefiles nach {\tt isabelle/src/HOLCF} zu kopieren, 
-es mu\ss\ au\ss erdem ROOT.ML
-folgenderma\ss en abge\"andert werden:\\
-Die Zeile 
-\begin{verbatim}
-init_thy_reader();
-\end{verbatim}
-wird ersetzt durch die Zeilen 
-\begin{verbatim}
-use "holcflogic.ML";
-use "thy_axioms.ML";
-use "thy_ops.ML";
-use "thy_syntax.ML";
-\end{verbatim}
-abschliessend wird die {\tt HOLCF}--Database neu erzeugt:\\
-{\tt make -f Makefile}\\
-(Vorraussetzung ist nat\"urlich, da\ss\ die {\tt ISABELLE...}--Environment
-Variablen korrekt, wie im Makefile beschrieben, gesetzt sind.)
-
-Die Installation ist damit abgeschlossen.
-
-
- 
\ No newline at end of file
diff -r b689656214ea -r 1e7621573d9c src/HOLCF/ax_ops/thy_syntax.ML
--- a/src/HOLCF/ax_ops/thy_syntax.ML	Wed Aug 06 01:18:31 1997 +0200
+++ b/src/HOLCF/ax_ops/thy_syntax.ML	Wed Aug 06 11:19:59 1997 +0200
@@ -2,13 +2,7 @@
     ID:         $Id$
     Author:     Tobias Mayr
 
-Installation of the additional theory file sections for HOLCF: axioms , ops 
-There's an elaborate but german description of this extension
-and a short english description of the new sections,
-write to mayrt@informatik.tu-muenchen.de.
-
-TODO:
-
+Additional thy file sections for HOLCF: axioms, ops.
 *)
 
 (* use "holcflogics.ML";