|
1274
|
1 |
|
|
|
2 |
Um diese Erweiterung zu installieren, gen\"ugt es nat\"urlich nicht, die
|
|
|
3 |
Sourcefiles nach {\tt isabelle/src/HOLCF} zu kopieren,
|
|
|
4 |
es mu\ss\ au\ss erdem ROOT.ML
|
|
|
5 |
folgenderma\ss en abge\"andert werden:\\
|
|
|
6 |
Die Zeile
|
|
|
7 |
\begin{verbatim}
|
|
|
8 |
init_thy_reader();
|
|
|
9 |
\end{verbatim}
|
|
|
10 |
wird ersetzt durch die Zeilen
|
|
|
11 |
\begin{verbatim}
|
|
|
12 |
use "holcflogic.ML";
|
|
|
13 |
use "thy_axioms.ML";
|
|
|
14 |
use "thy_ops.ML";
|
|
|
15 |
use "thy_syntax.ML";
|
|
|
16 |
\end{verbatim}
|
|
|
17 |
abschliessend wird die {\tt HOLCF}--Database neu erzeugt:\\
|
|
|
18 |
{\tt make -f Makefile}\\
|
|
|
19 |
(Vorraussetzung ist nat\"urlich, da\ss\ die {\tt ISABELLE...}--Environment
|
|
|
20 |
Variablen korrekt, wie im Makefile beschrieben, gesetzt sind.)
|
|
|
21 |
|
|
|
22 |
Die Installation ist damit abgeschlossen.
|
|
|
23 |
|
|
|
24 |
|
|
|
25 |
|