nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Updated READMEs after session renaming.

This commit is contained in:
Achim D. Brucker 2023-04-15 16:55:15 +01:00
parent 9318ea55a0
commit d277fa2aed
2 changed files with 7 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
README.md
View File

@ -35,7 +35,7 @@ Isabelle/DOF is currently consisting out of two AFP entries:
* [Isabelle_DOF:](https://www.isa-afp.org/entries/Isabelle_DOF.html) This entry
contains the Isabelle/DOF system itself, including the Isabelle/DOF manual.
* [Isabelle_DOF-Example-Scholarly_Paper:](https://www.isa-afp.org/entries/Isabelle_DOF-Example-Scholarly_Paper.html)
* [Isabelle_DOF-Example-I:](https://www.isa-afp.org/entries/Isabelle_DOF-Example-I.html)
This entry contains an example of an academic paper written using the
Isabelle/DOF system.
@ -77,11 +77,11 @@ repository of Isabelle/DOF (installing Isabelle/DOF as a component to your
Isabelle system).
Assuming that your current directory contains the example academic paper in the
subdirectory ``Isabelle_DOF-Example-Scholarly_Paper/``, you can open it similar
subdirectory ``Isabelle_DOF-Example-I/``, you can open it similar
to any standard Isabelle theory:
```console
isabelle jedit -l Isabelle_DOF Isabelle_DOF-Example-Scholarly_Paper/IsaDofApplications.thy
isabelle jedit -l Isabelle_DOF Isabelle_DOF-Example-I/IsaDofApplications.thy
```
This will open an example of a scientific paper using the pre-compiled session
@ -90,7 +90,7 @@ defined in the ``Isabelle_DOF`` session. If you want to edit the ontology defin
just open the theory file with the session ``Functional-Automata``:
```console
isabelle jedit -l Functional-Automata Isabelle_DOF-Example-Scholarly_Paper/IsaDofApplications.thy
isabelle jedit -l Functional-Automata Isabelle_DOF-Example-I/IsaDofApplications.thy
```
While this gives you more flexibility, it might "clutter" your editing
@ -109,7 +109,7 @@ in a subdirectory:
* [Isabelle_DOF](./Isabelle_DOF/): This is the main session, providing the
Isabelle/DOF system. Furthermore, this session is currently under
consideration for a submission to the AFP.
* [Isabelle_DOF-Example-Scholarly_Paper](./Isabelle_DOF-Example-Scholarly_Paper/):
* [Isabelle_DOF-Example-I](./Isabelle_DOF-Example-I/):
This session provides an example document written Isabelle/DOF. It only
requires the core ontologies provided by the ``Isabelle_DOF`` session.
Furthermore, this session is currently under consideration for a submission to

4
README_DEVELOPMENT.md
View File

@ -28,10 +28,10 @@ complete AFP. For this, please follow the instructions given at
<!--
As Isabelle session names need to be
unique, you will need to disable the entries ``Isabelle_DOF`` and
``Isabelle_DOF-Example-Scholarly_Paper`` provided as part of the AFP. For this,
``Isabelle_DOF-Example-I`` provided as part of the AFP. For this,
you will need to edit the file ``$AFP/thys/ROOTS`` (where ``$AFP`` refers to the
directory in which you installed the AFP) and delete the two entries
``Isabelle_DOF`` and ``Isabelle_DOF-Example-Scholarly_Paper``.
``Isabelle_DOF`` and ``Isabelle_DOF-Example-I``.
-->
For the development version of Isabelle, installing the complete AFP