From eda8535b1c0fa0a87938f2d6e65836b5498bf9bf Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Thu, 6 Dec 2018 12:31:12 +0100
Subject: [PATCH] - changed back ROOTS - IsaDof_Manual Monitor should be
 report.

---
 Isa_DOF.thy                                       | 15 ++++++++++++++-
 ROOTS                                             |  3 ++-
 examples/conceptual/Concept_ExampleInvariant.thy  |  2 +-
 .../IsaDof_Manual/00_Frontmatter.thy              |  2 +-
 4 files changed, 18 insertions(+), 4 deletions(-)

diff --git a/Isa_DOF.thy b/Isa_DOF.thy
index 3645256..e5f83da 100644
--- a/Isa_DOF.thy
+++ b/Isa_DOF.thy
@@ -1549,8 +1549,21 @@ val _ =
 end (* struct *)
 \<close>  
 
-ML\<open>
+text\<open> @{term "a + b"}\<close>
 
+text\<open>copied from @{file "$ISABELLE_HOME/src/Pure/Thy/thy_output.ML"} \<close>
+ML\<open> (* copy from *)
+fun basic_entities name scan pretty =
+  Thy_Output.antiquotation name scan (fn {source, context = ctxt, ...} =>
+    Thy_Output.output ctxt o Thy_Output.maybe_pretty_source pretty ctxt source);
+
+fun basic_entity name scan = basic_entities name (scan >> single);
+
+Thy_Output.pretty_term;
+
+(*
+  basic_entity @{binding term} (Term_Style.parse -- Args.term) pretty_term_style 
+*)
 \<close>
 
 section\<open> Testing and Validation \<close>
diff --git a/ROOTS b/ROOTS
index 54bb305..39d7ac7 100644
--- a/ROOTS
+++ b/ROOTS
@@ -1,2 +1,3 @@
-AFP-contribs
+AFP-contribs/Regular-Sets
+AFP-contribs/Functional-Automata
 examples
diff --git a/examples/conceptual/Concept_ExampleInvariant.thy b/examples/conceptual/Concept_ExampleInvariant.thy
index 114318e..debfb1b 100644
--- a/examples/conceptual/Concept_ExampleInvariant.thy
+++ b/examples/conceptual/Concept_ExampleInvariant.thy
@@ -85,7 +85,7 @@ text*[c1::C, x = "''beta''"]  \<open> ... suspendisse non arcu malesuada mollis,
 
 text*[d1::E, a1 = "X3"]       \<open> ... phasellus amet id massa nunc, pede suscipit repellendus, ... \<close>
     
-text*[c2::C, x = "''delta''"] \<open> ... in ut tortor eleifend augue pretium consectetuer...  \<close>
+text*[c2:: C, x = "''delta''"] \<open> ... in ut tortor eleifend augue pretium consectetuer...  \<close>
 
 section*[f::E]                \<open> Lectus accumsan velit ultrices, ... }\<close>
 
diff --git a/examples/technical_report/IsaDof_Manual/00_Frontmatter.thy b/examples/technical_report/IsaDof_Manual/00_Frontmatter.thy
index cf587d5..4af325e 100644
--- a/examples/technical_report/IsaDof_Manual/00_Frontmatter.thy
+++ b/examples/technical_report/IsaDof_Manual/00_Frontmatter.thy
@@ -3,7 +3,7 @@ theory "00_Frontmatter"
   imports "../../../ontologies/technical_report"
 begin
 
-open_monitor*[this::article] 
+open_monitor*[this::report] 
 
 (*>*)