--- 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
--- 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";