forked from Isabelle_DOF/Isabelle_DOF
Added crucial installation comment in the README concerning the installation
This commit is contained in:
parent
f6aec1f0b1
commit
1f50068373
11
README.md
11
README.md
|
@ -16,10 +16,21 @@ argument to the ``install`` script:
|
||||||
```console
|
```console
|
||||||
foo@bar:~$ ./install /usr/local/Isabelle2016-1/bin/isabelle
|
foo@bar:~$ ./install /usr/local/Isabelle2016-1/bin/isabelle
|
||||||
```
|
```
|
||||||
|
or likewise:
|
||||||
|
```console
|
||||||
|
foo@bar:~$ ./install /usr/local/Isabelle2017/bin/isabelle
|
||||||
|
```
|
||||||
|
|
||||||
The DOF-plugin will be installed in the Isabelle user directory
|
The DOF-plugin will be installed in the Isabelle user directory
|
||||||
(the exact location depends on the Isabelle version).
|
(the exact location depends on the Isabelle version).
|
||||||
|
|
||||||
|
Additionally, you have to replace the file
|
||||||
|
```Isabelle2017/src/Pure/Thy/thy_output.ML```
|
||||||
|
by the file you find in the Isabelle_DOF-distribution:
|
||||||
|
```patches/thy_output.ML```
|
||||||
|
When starting up, Isabelle will recompile itself and integrating this
|
||||||
|
file (which modifies about 10 lines in the LaTeX generator...).
|
||||||
|
|
||||||
## Usage
|
## Usage
|
||||||
|
|
||||||
The DOF-plugin provides an alternative to Isabelle's ``mkroot`` command.
|
The DOF-plugin provides an alternative to Isabelle's ``mkroot`` command.
|
||||||
|
|
Loading…
Reference in New Issue