From 458f07647321631f63c9d31a3773c837fbef7762 Mon Sep 17 00:00:00 2001
From: "Achim D. Brucker" <adbrucker@0x5f.org>
Date: Sun, 28 Jul 2019 11:53:39 +0100
Subject: [PATCH] Fixed lstisar syntax.

---
 .../Isabelle_DOF-Manual/04_RefMan.thy         | 26 +++++++++----------
 1 file changed, 13 insertions(+), 13 deletions(-)

diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
index 5046a44..80a4b81 100644
--- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
+++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
@@ -298,7 +298,7 @@ text\<open>To express the dependencies between text elements to the formal
   \<^emph>\<open>inside\<close> the HOL type system.  We do, however, not reflect the data of
   these types. They are just declared abstract types, 
   ``inhabited'' by special constant symbols carrying strings, for
-  example of the format \inlineisar+<AT>{thm <string>}+. When HOL
+  example of the format \inlineisar+<@>{thm <string>}+. When HOL
   expressions were used to denote values of \inlineisar+doc_class+
   instance attributes, this requires additional checks after
   conventional type-checking that this string represents actually a
@@ -307,15 +307,15 @@ text\<open>To express the dependencies between text elements to the formal
   attribute in the previous section is the power of the ODL: here, we model
   a relation between \<^emph>\<open>claims\<close> and \<^emph>\<open>results\<close> which may be a
   formal, machine-check theorem of type \inlinesml+thm+ denoted by, for
-  example: \inlineisar+property = "[<AT>{thm ''system_is_safe''}]"+ in a
+  example: \inlineisar+property = "[<@>{thm ''system_is_safe''}]"+ in a
   system context \inlineisar+\<theta>+ where this theorem is
   established. Similarly, attribute values like 
-  \inlineisar+property = "<AT>{term \<Open>A \<leftrightarrow> B\<Close>}"+
+  \inlineisar+property = "<@>{term \<Open>A \<leftrightarrow> B\<Close>}"+
   require that the HOL-string \inlineisar+A \<leftrightarrow> B+ is 
   again type-checked and represents indeed a formula in $\theta$. Another instance of 
   this process, which we call \<open>second-level type-checking\<close>, are term-constants
   generated from the ontology such as 
-  \inlineisar+<AT>{definition <string>}+. For the latter, the argument string
+  \inlineisar+<@>{definition <string>}+. For the latter, the argument string
   must be checked that it  represents a reference to a text-element
   having the type \inlineisar+definition+ according to the ontology in @{example "odl-design"}.\<close>
 
@@ -403,11 +403,11 @@ class invariants. A formulation, in SML, of the first class-invariant
 in \autoref{sec:class_inv} is straight-forward:
 \begin{sml}
 fun check_result_inv oid {is_monitor:bool} ctxt =
-  let val kind = compute_attr_access ctxt "kind" oid <AT>{here} <AT>{here}
-      val prop = compute_attr_access ctxt "property" oid <AT>{here} <AT>{here}
+  let val kind = compute_attr_access ctxt "kind" oid <@>{here} <@>{here}
+      val prop = compute_attr_access ctxt "property" oid <@>{here} <@>{here}
       val tS = HOLogic.dest_list prop
   in  case kind_term of
-       <AT>{term "proof"} => if not(null tS) then true
+       <@>{term "proof"} => if not(null tS) then true
                           else error("class result invariant violation")
       | _ => false
   end
@@ -419,7 +419,7 @@ The \inlinesml{setup}-command (last line) registers the
 activates any creation or modification of an instance of
 \inlineisar+result+.  We cannot replace \inlineisar+compute_attr_access+
 by the corresponding antiquotation
-\inlineisar+<AT>{docitem_value kind::oid}+, since \inlineisar+oid+ is
+\inlineisar+<@>{docitem_value kind::oid}+, since \inlineisar+oid+ is
 bound to a variable here and can therefore not be statically expanded.
 
 Isabelle's code generator can in principle generate class invariant code
@@ -549,22 +549,22 @@ subsection\<open>Editing Documents with Ontology Meta-Data: Inner Syntax\<close>
 text\<open>We continue our running example as follows:
 \begin{isar}[mathescape]
 text*[d1::definition]\<Open>
-  We define the water level <AT>{term "level"} of a system state
-  <AT>{term "\<sigma>"} of the steam boiler as follows: 
+  We define the water level <@>{term "level"} of a system state
+  <@>{term "\<sigma>"} of the steam boiler as follows: 
 \<Close>
 definition level :: "state \<rightarrow> real" where
           "level \<sigma> =  level0 + ..." 
 update_instance*[d1::definition,
-                 property += "[<AT>{term ''level \<sigma> =  level0 + ...''}]"]
+                 property += "[<@>{term ''level \<sigma> =  level0 + ...''}]"]
 
 text*[only::result,evidence="proof"]\<Open>
-  The water level is never lower than <AT>{term "level0"}:
+  The water level is never lower than <@>{term "level0"}:
 \<Close>
 theorem level_always_above_level_0: "\<forall> \<sigma>. level \<sigma> \<geq> level0"
   unfolding level_def
   by auto
 update_instance*[only::result,
-                 property += "[<AT>{thm ''level_always_above_level_0''}]"]
+                 property += "[<@>{thm ''level_always_above_level_0''}]"]
 \end{isar}
 \<close>
 text\<open>