Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Converted \inlinesml{...}.

This commit is contained in:
Achim D. Brucker 2021-02-02 12:22:35 +00:00
parent 2d3e521296
commit d605e23218
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
examples/technical_report/Isabelle_DOF-Manual/02_Background.thy
View File

@ -47,7 +47,7 @@ The current system framework offers moreover the following features:
The Isabelle system architecture shown in @{docitem \<open>architecture\<close>} comes with many layers, The Isabelle system architecture shown in @{docitem \<open>architecture\<close>} comes with many layers,
with Standard ML (SML) at the bottom layer as implementation language. The architecture actually with Standard ML (SML) at the bottom layer as implementation language. The architecture actually
foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which resides in the SML structure \inlinesml{Context}. foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which resides in the SML structure\<^boxed_sml>\<open>Context\<close>.
This structure provides a kind of container called \<^emph>\<open>context\<close> providing an identity, an This structure provides a kind of container called \<^emph>\<open>context\<close> providing an identity, an
ancestor-list as well as typed, user-defined state for components (plugins) such as \<^isadof>. 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 On top of the latter, the LCF-Kernel, tactics, automated proof procedures as well as specific