From 36ff213103d4ac6ef8e3d519196d53c938e2d094 Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Sun, 21 Jul 2019 16:35:08 +0200
Subject: [PATCH] more experiments

---
 examples/technical_report/IsaDof_Manual/04_RefMan.thy | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/examples/technical_report/IsaDof_Manual/04_RefMan.thy b/examples/technical_report/IsaDof_Manual/04_RefMan.thy
index 1a0a911..0bf3258 100644
--- a/examples/technical_report/IsaDof_Manual/04_RefMan.thy
+++ b/examples/technical_report/IsaDof_Manual/04_RefMan.thy
@@ -555,7 +555,7 @@ In a high-level syntax, this type of constraints could be expressed, \eg, by:
 \begin{isar}
 \<forall> x \<in> result. x@kind = proof \<leftrightarrow> x@kind \<noteq> []
 \<forall> x \<in> conclusion. \<forall> y \<in> Domain(x@establish)
-                  \<rightarrow> \<exists> y\<in> Range(x@establish). (y,z) \<in> x@establish
+                  \<rightarrow> \<exists> y \<in> Range(x@establish). (y,z) \<in> x@establish
 \<forall> x \<in> introduction. finite(x@authored_by)
 \end{isar}
 @{cartouche [display=true] \<open>  
@@ -573,7 +573,8 @@ these document classes.  All specified constraints are already checked
 in the IDE of \dof while editing; it is however possible to delay a
 final error message till the closing of a monitor (see next
 section). The third constraint enforces that the
-user sets the \inlineisar+authored_by+ set, otherwise an error will be
+user sets the \<open>authored_by\<close> set, otherwise an error will be
+%%user sets the \inlineisar+authored_by+ set, otherwise an error will be
 reported.
 \<close>