diff --git a/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy b/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy index 6ae74a7..820b971 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy @@ -47,7 +47,7 @@ The current system framework offers moreover the following features: The Isabelle system architecture shown in @{docitem \architecture\} comes with many layers, with Standard ML (SML) at the bottom layer as implementation language. The architecture actually -foresees a \<^emph>\Nano-Kernel\ (our terminology) which resides in the SML structure \inlinesml{Context}. +foresees a \<^emph>\Nano-Kernel\ (our terminology) which resides in the SML structure\<^boxed_sml>\Context\. This structure provides a kind of container called \<^emph>\context\ providing an identity, an ancestor-list as well as typed, user-defined state for components (plugins) such as \<^isadof>. On top of the latter, the LCF-Kernel, tactics, automated proof procedures as well as specific