equal
deleted
inserted
replaced
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 |
|