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

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

diff --git a/examples/technical_report/IsaDof_Manual/04_RefMan.thy b/examples/technical_report/IsaDof_Manual/04_RefMan.thy
index f0ed287..1a0a911 100644
--- a/examples/technical_report/IsaDof_Manual/04_RefMan.thy
+++ b/examples/technical_report/IsaDof_Manual/04_RefMan.thy
@@ -565,8 +565,10 @@ In a high-level syntax, this type of constraints could be expressed, \eg, by:
 (* 3 *)     \<forall> x \<in> introduction. finite(x@authored_by)
 \<close>}
 \fixme{experiment... }
-where \inlineisar+result+, \inlineisar+conclusion+, and
-\inlineisar+introduction+ are the set of all possible instances of
+%% where \inlineisar+result+, \inlineisar+conclusion+, and
+%% 
+where \<open>result\<close>, \<open>conclusion\<close>, and
+\<open>introduction\<close> are the set of all possible instances of
 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