From d85a1340f7888f508e3e9c69c2de60c9a35abb5c Mon Sep 17 00:00:00 2001
From: "Achim D. Brucker" <adbrucker@0x5f.org>
Date: Sun, 6 Jan 2019 18:43:23 +0000
Subject: [PATCH] Documented interactive use of examples.

---
 README.md | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/README.md b/README.md
index 3d30818b..6f411ea7 100644
--- a/README.md
+++ b/README.md
@@ -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: