src/Doc/Implementation/Integration.thy

 chapter \<open>System integration\<close>
 
 section \<open>Isar toplevel \label{sec:isar-toplevel}\<close>
 
 text \<open>
-  The Isar \emph{toplevel state} represents the outermost configuration that
+  The Isar \<^emph>\<open>toplevel state\<close> represents the outermost configuration that
   is transformed by a sequence of transitions (commands) within a theory body.
   This is a pure value with pure functions acting on it in a timeless and
   stateless manner. Historically, the sequence of transitions was wrapped up
   as sequential command loop, such that commands are applied one-by-one. In
   contemporary Isabelle/Isar, processing toplevel commands usually works in

 
 text \<open>
   In batch mode and within dumped logic images, the theory database maintains
   a collection of theories as a directed acyclic graph. A theory may refer to
   other theories as @{keyword "imports"}, or to auxiliary files via special
-  \emph{load commands} (e.g.\ @{command ML_file}). For each theory, the base
-  directory of its own theory file is called \emph{master directory}: this is
+  \<^emph>\<open>load commands\<close> (e.g.\ @{command ML_file}). For each theory, the base
+  directory of its own theory file is called \<^emph>\<open>master directory\<close>: this is
   used as the relative location to refer to other files from that theory.
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}