Documented interactive use of examples.

This commit is contained in:
Achim D. Brucker 2019-01-06 18:43:23 +00:00
parent b91377edbd
commit d85a1340f7
1 changed files with 25 additions and 0 deletions

View File

@ -51,6 +51,30 @@ The installer will
## Usage
### Opening an Example
If you want to work with or extend one of the examples, e.g., you can
open it similar to any standard Isabelle theory:
```console
isabelle jedit -d . -l Isabelle_DOF examples/scholarly_paper/2018_cicm/IsaDofApplications.thy
```
This will open an example of a scientific paper using the pre-compiled
session ``Isabelle_DOF``, i.e., you will not be able to edit the
ontology definitions. If you want to edit the ontology definition,
just open the theory file with the default HOL session:
```console
isabelle jedit -d . -l Isabelle_DOF examples/scholarly_paper/2018_cicm/IsaDofApplications.thy
```
While this gives you more flexibility, it might "clutter" your editing
experience, as a lot of internal theories are loaded into Isabelle's
editor.
### Creating a New Project
The DOF-plugin provides an alternative to Isabelle's ``mkroot`` command.
Isabelle projects that use DOF need to be created using
```console
@ -97,6 +121,7 @@ website and either copy it in you ``texmf`` directory or the ``root``
folder. In the latter case, you also need to add it in the ``ROOT`` file
as dependency.
## Team
Main contacts: