doc-src/Locales/Locales/document/Examples3.tex

   \label{sec:local-interpretation}%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-In the above example, the fact that \isa{op\ {\isasymle}} is a partial
+In the above example, the fact that \isa{op\ {\isaliteral{5C3C6C653E}{\isasymle}}} is a partial
   order for the integers was used in the second goal to
-  discharge the premise in the definition of \isa{op\ {\isasymsqsubset}}.  In
+  discharge the premise in the definition of \isa{op\ {\isaliteral{5C3C73717375627365743E}{\isasymsqsubset}}}.  In
   general, proofs of the equations not only may involve definitions
   from the interpreted locale but arbitrarily complex arguments in the
   context of the locale.  Therefore is would be convenient to have the
   interpreted locale conclusions temporary available in the proof.
   This can be achieved by a locale interpretation in the proof body.

 \ \ %
 \endisadelimvisible
 %
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
-\ int{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ int{\isaliteral{3A}{\isacharcolon}}\ partial{\isaliteral{5F}{\isacharunderscore}}order\ {\isaliteral{22}{\isachardoublequoteopen}}op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \ \ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}partial{\isaliteral{5F}{\isacharunderscore}}order{\isaliteral{2E}{\isachardot}}less\ op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}int{\isaliteral{29}{\isacharparenright}}\ y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3C}{\isacharless}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \ \ \isacommand{proof}\isamarkupfalse%
-\ {\isacharminus}\isanewline
+\ {\isaliteral{2D}{\isacharminus}}\isanewline
 \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}partial{\isacharunderscore}order\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}partial{\isaliteral{5F}{\isacharunderscore}}order\ {\isaliteral{28}{\isacharparenleft}}op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
-\ unfold{\isacharunderscore}locales\ auto\isanewline
+\ unfold{\isaliteral{5F}{\isacharunderscore}}locales\ auto\isanewline
 \ \ \ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{interpret}\isamarkupfalse%
-\ int{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}int{\isacharcomma}\ int{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
+\ int{\isaliteral{3A}{\isacharcolon}}\ partial{\isaliteral{5F}{\isacharunderscore}}order\ {\isaliteral{22}{\isachardoublequoteopen}}op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5B}{\isacharbrackleft}}int{\isaliteral{2C}{\isacharcomma}}\ int{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
 \isanewline
 \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}partial{\isaliteral{5F}{\isacharunderscore}}order{\isaliteral{2E}{\isachardot}}less\ op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}int{\isaliteral{29}{\isacharparenright}}\ y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3C}{\isacharless}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
-\ int{\isachardot}less{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ int{\isaliteral{2E}{\isachardot}}less{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse%
 \ auto\isanewline
 \ \ \isacommand{qed}\isamarkupfalse%
 %
 \endisatagvisible
 {\isafoldvisible}%

 \begin{isamarkuptext}%
 The inner interpretation is immediate from the preceding fact
   and proved by assumption (Isar short hand ``.'').  It enriches the
   local proof context by the theorems
   also obtained in the interpretation from Section~\ref{sec:po-first},
-  and \isa{int{\isachardot}less{\isacharunderscore}def} may directly be used to unfold the
+  and \isa{int{\isaliteral{2E}{\isachardot}}less{\isaliteral{5F}{\isacharunderscore}}def} may directly be used to unfold the
   definition.  Theorems from the local interpretation disappear after
   leaving the proof context --- that is, after the succeeding
   \isakeyword{next} or \isakeyword{qed} statement.%
 \end{isamarkuptext}%
 \isamarkuptrue%

 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
 Further interpretations are necessary for
-  the other locales.  In \isa{lattice} the operations~\isa{{\isasymsqinter}}
-  and~\isa{{\isasymsqunion}} are substituted by \isa{min}
+  the other locales.  In \isa{lattice} the operations~\isa{{\isaliteral{5C3C7371696E7465723E}{\isasymsqinter}}}
+  and~\isa{{\isaliteral{5C3C7371756E696F6E3E}{\isasymsqunion}}} are substituted by \isa{min}
   and \isa{max}.  The entire proof for the
   interpretation is reproduced to give an example of a more
   elaborate interpretation proof.  Note that the equations are named
   so they can be used in a later example.%
 \end{isamarkuptext}%

 \ \ %
 \endisadelimvisible
 %
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
-\ int{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{where}\ int{\isacharunderscore}min{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \isakeyword{and}\ int{\isacharunderscore}max{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ max\ x\ y{\isachardoublequoteclose}\isanewline
+\ int{\isaliteral{3A}{\isacharcolon}}\ lattice\ {\isaliteral{22}{\isachardoublequoteopen}}op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \ \ \isakeyword{where}\ int{\isaliteral{5F}{\isacharunderscore}}min{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}lattice{\isaliteral{2E}{\isachardot}}meet\ op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}int{\isaliteral{29}{\isacharparenright}}\ y\ {\isaliteral{3D}{\isacharequal}}\ min\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \ \ \ \ \isakeyword{and}\ int{\isaliteral{5F}{\isacharunderscore}}max{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}lattice{\isaliteral{2E}{\isachardot}}join\ op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}int{\isaliteral{29}{\isacharparenright}}\ y\ {\isaliteral{3D}{\isacharequal}}\ max\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \ \ \isacommand{proof}\isamarkupfalse%
-\ {\isacharminus}\isanewline
+\ {\isaliteral{2D}{\isacharminus}}\isanewline
 \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}lattice\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}%
+\ {\isaliteral{22}{\isachardoublequoteopen}}lattice\ {\isaliteral{28}{\isacharparenleft}}op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
 \begin{isamarkuptxt}%
 \normalsize We have already shown that this is a partial
 	order,%
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ unfold{\isacharunderscore}locales%
+\ unfold{\isaliteral{5F}{\isacharunderscore}}locales%
 \begin{isamarkuptxt}%
 \normalsize hence only the lattice axioms remain to be
 	shown.
         \begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ {\isasymexists}inf{\isachardot}\ partial{\isacharunderscore}order{\isachardot}is{\isacharunderscore}inf\ op\ {\isasymle}\ x\ y\ inf\isanewline
-\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ {\isasymexists}sup{\isachardot}\ partial{\isacharunderscore}order{\isachardot}is{\isacharunderscore}sup\ op\ {\isasymle}\ x\ y\ sup%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}inf{\isaliteral{2E}{\isachardot}}\ partial{\isaliteral{5F}{\isacharunderscore}}order{\isaliteral{2E}{\isachardot}}is{\isaliteral{5F}{\isacharunderscore}}inf\ op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ x\ y\ inf\isanewline
+\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}sup{\isaliteral{2E}{\isachardot}}\ partial{\isaliteral{5F}{\isacharunderscore}}order{\isaliteral{2E}{\isachardot}}is{\isaliteral{5F}{\isacharunderscore}}sup\ op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ x\ y\ sup%
 \end{isabelle}
-	By \isa{is{\isacharunderscore}inf} and \isa{is{\isacharunderscore}sup},%
+	By \isa{is{\isaliteral{5F}{\isacharunderscore}}inf} and \isa{is{\isaliteral{5F}{\isacharunderscore}}sup},%
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}unfold\ int{\isachardot}is{\isacharunderscore}inf{\isacharunderscore}def\ int{\isachardot}is{\isacharunderscore}sup{\isacharunderscore}def{\isacharparenright}%
+\ {\isaliteral{28}{\isacharparenleft}}unfold\ int{\isaliteral{2E}{\isachardot}}is{\isaliteral{5F}{\isacharunderscore}}inf{\isaliteral{5F}{\isacharunderscore}}def\ int{\isaliteral{2E}{\isachardot}}is{\isaliteral{5F}{\isacharunderscore}}sup{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}%
 \begin{isamarkuptxt}%
 \normalsize the goals are transformed to these
 	statements:
 	\begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ {\isasymexists}inf{\isasymle}x{\isachardot}\ inf\ {\isasymle}\ y\ {\isasymand}\ {\isacharparenleft}{\isasymforall}z{\isachardot}\ z\ {\isasymle}\ x\ {\isasymand}\ z\ {\isasymle}\ y\ {\isasymlongrightarrow}\ z\ {\isasymle}\ inf{\isacharparenright}\isanewline
-\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ {\isasymexists}sup{\isasymge}x{\isachardot}\ y\ {\isasymle}\ sup\ {\isasymand}\ {\isacharparenleft}{\isasymforall}z{\isachardot}\ x\ {\isasymle}\ z\ {\isasymand}\ y\ {\isasymle}\ z\ {\isasymlongrightarrow}\ sup\ {\isasymle}\ z{\isacharparenright}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}inf{\isaliteral{5C3C6C653E}{\isasymle}}x{\isaliteral{2E}{\isachardot}}\ inf\ {\isaliteral{5C3C6C653E}{\isasymle}}\ y\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}z{\isaliteral{2E}{\isachardot}}\ z\ {\isaliteral{5C3C6C653E}{\isasymle}}\ x\ {\isaliteral{5C3C616E643E}{\isasymand}}\ z\ {\isaliteral{5C3C6C653E}{\isasymle}}\ y\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ z\ {\isaliteral{5C3C6C653E}{\isasymle}}\ inf{\isaliteral{29}{\isacharparenright}}\isanewline
+\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}sup{\isaliteral{5C3C67653E}{\isasymge}}x{\isaliteral{2E}{\isachardot}}\ y\ {\isaliteral{5C3C6C653E}{\isasymle}}\ sup\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}z{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C6C653E}{\isasymle}}\ z\ {\isaliteral{5C3C616E643E}{\isasymand}}\ y\ {\isaliteral{5C3C6C653E}{\isasymle}}\ z\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ sup\ {\isaliteral{5C3C6C653E}{\isasymle}}\ z{\isaliteral{29}{\isacharparenright}}%
 \end{isabelle}
 	This is Presburger arithmetic, which can be solved by the
         method \isa{arith}.%
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
-\ arith{\isacharplus}%
+\ arith{\isaliteral{2B}{\isacharplus}}%
 \begin{isamarkuptxt}%
 \normalsize In order to show the equations, we put ourselves
       in a situation where the lattice theorems can be used in a
       convenient way.%
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \ \ \ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{interpret}\isamarkupfalse%
-\ int{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
+\ int{\isaliteral{3A}{\isacharcolon}}\ lattice\ {\isaliteral{22}{\isachardoublequoteopen}}op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
 \isanewline
 \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}lattice{\isaliteral{2E}{\isachardot}}meet\ op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}int{\isaliteral{29}{\isacharparenright}}\ y\ {\isaliteral{3D}{\isacharequal}}\ min\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}bestsimp\ simp{\isacharcolon}\ int{\isachardot}meet{\isacharunderscore}def\ int{\isachardot}is{\isacharunderscore}inf{\isacharunderscore}def{\isacharparenright}\isanewline
+\ {\isaliteral{28}{\isacharparenleft}}bestsimp\ simp{\isaliteral{3A}{\isacharcolon}}\ int{\isaliteral{2E}{\isachardot}}meet{\isaliteral{5F}{\isacharunderscore}}def\ int{\isaliteral{2E}{\isachardot}}is{\isaliteral{5F}{\isacharunderscore}}inf{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline
 \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ max\ x\ y{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}lattice{\isaliteral{2E}{\isachardot}}join\ op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}int{\isaliteral{29}{\isacharparenright}}\ y\ {\isaliteral{3D}{\isacharequal}}\ max\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}bestsimp\ simp{\isacharcolon}\ int{\isachardot}join{\isacharunderscore}def\ int{\isachardot}is{\isacharunderscore}sup{\isacharunderscore}def{\isacharparenright}\isanewline
+\ {\isaliteral{28}{\isacharparenleft}}bestsimp\ simp{\isaliteral{3A}{\isacharcolon}}\ int{\isaliteral{2E}{\isachardot}}join{\isaliteral{5F}{\isacharunderscore}}def\ int{\isaliteral{2E}{\isachardot}}is{\isaliteral{5F}{\isacharunderscore}}sup{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline
 \ \ \isacommand{qed}\isamarkupfalse%
 %
 \endisatagvisible
 {\isafoldvisible}%
 %
 \isadelimvisible
 %
 \endisadelimvisible
 %
 \begin{isamarkuptext}%
-Next follows that \isa{op\ {\isasymle}} is a total order, again for
+Next follows that \isa{op\ {\isaliteral{5C3C6C653E}{\isasymle}}} is a total order, again for
   the integers.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isadelimvisible
 \ \ %
 \endisadelimvisible
 %
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
-\ int{\isacharcolon}\ total{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ int{\isaliteral{3A}{\isacharcolon}}\ total{\isaliteral{5F}{\isacharunderscore}}order\ {\isaliteral{22}{\isachardoublequoteopen}}op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \ \ \ \ \isacommand{by}\isamarkupfalse%
-\ unfold{\isacharunderscore}locales\ arith%
+\ unfold{\isaliteral{5F}{\isacharunderscore}}locales\ arith%
 \endisatagvisible
 {\isafoldvisible}%
 %
 \isadelimvisible
 %

 \begin{table}
 \hrule
 \vspace{2ex}
 \begin{center}
 \begin{tabular}{l}
-  \isa{int{\isachardot}less{\isacharunderscore}def} from locale \isa{partial{\isacharunderscore}order}: \\
-  \quad \isa{{\isacharparenleft}{\isacharquery}x\ {\isacharless}\ {\isacharquery}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharquery}x\ {\isasymle}\ {\isacharquery}y\ {\isasymand}\ {\isacharquery}x\ {\isasymnoteq}\ {\isacharquery}y{\isacharparenright}} \\
-  \isa{int{\isachardot}meet{\isacharunderscore}left} from locale \isa{lattice}: \\
-  \quad \isa{min\ {\isacharquery}x\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}x} \\
-  \isa{int{\isachardot}join{\isacharunderscore}distr} from locale \isa{distrib{\isacharunderscore}lattice}: \\
-  \quad \isa{max\ {\isacharquery}x\ {\isacharparenleft}min\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ min\ {\isacharparenleft}max\ {\isacharquery}x\ {\isacharquery}y{\isacharparenright}\ {\isacharparenleft}max\ {\isacharquery}x\ {\isacharquery}z{\isacharparenright}} \\
-  \isa{int{\isachardot}less{\isacharunderscore}total} from locale \isa{total{\isacharunderscore}order}: \\
-  \quad \isa{{\isacharquery}x\ {\isacharless}\ {\isacharquery}y\ {\isasymor}\ {\isacharquery}x\ {\isacharequal}\ {\isacharquery}y\ {\isasymor}\ {\isacharquery}y\ {\isacharless}\ {\isacharquery}x}
+  \isa{int{\isaliteral{2E}{\isachardot}}less{\isaliteral{5F}{\isacharunderscore}}def} from locale \isa{partial{\isaliteral{5F}{\isacharunderscore}}order}: \\
+  \quad \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{3F}{\isacharquery}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{3F}{\isacharquery}}y\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{3F}{\isacharquery}}y{\isaliteral{29}{\isacharparenright}}} \\
+  \isa{int{\isaliteral{2E}{\isachardot}}meet{\isaliteral{5F}{\isacharunderscore}}left} from locale \isa{lattice}: \\
+  \quad \isa{min\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{3F}{\isacharquery}}y\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{3F}{\isacharquery}}x} \\
+  \isa{int{\isaliteral{2E}{\isachardot}}join{\isaliteral{5F}{\isacharunderscore}}distr} from locale \isa{distrib{\isaliteral{5F}{\isacharunderscore}}lattice}: \\
+  \quad \isa{max\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{28}{\isacharparenleft}}min\ {\isaliteral{3F}{\isacharquery}}y\ {\isaliteral{3F}{\isacharquery}}z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ min\ {\isaliteral{28}{\isacharparenleft}}max\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{3F}{\isacharquery}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}max\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{3F}{\isacharquery}}z{\isaliteral{29}{\isacharparenright}}} \\
+  \isa{int{\isaliteral{2E}{\isachardot}}less{\isaliteral{5F}{\isacharunderscore}}total} from locale \isa{total{\isaliteral{5F}{\isacharunderscore}}order}: \\
+  \quad \isa{{\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{3F}{\isacharquery}}y\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}y\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{3F}{\isacharquery}}y\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{3F}{\isacharquery}}x}
 \end{tabular}
 \end{center}
 \hrule
-\caption{Interpreted theorems for~\isa{{\isasymle}} on the integers.}
+\caption{Interpreted theorems for~\isa{{\isaliteral{5C3C6C653E}{\isasymle}}} on the integers.}
 \label{tab:int-lattice}
 \end{table}
 
 \begin{itemize}
 \item
-  Locale \isa{distrib{\isacharunderscore}lattice} was also interpreted.  Since the
+  Locale \isa{distrib{\isaliteral{5F}{\isacharunderscore}}lattice} was also interpreted.  Since the
   locale hierarchy reflects that total orders are distributive
   lattices, the interpretation of the latter was inserted
   automatically with the interpretation of the former.  In general,
   interpretation traverses the locale hierarchy upwards and interprets
   all encountered locales, regardless whether imported or proved via
   the \isakeyword{sublocale} command.  Existing interpretations are
   skipped avoiding duplicate work.
 \item
-  The predicate \isa{op\ {\isacharless}} appears in theorem \isa{int{\isachardot}less{\isacharunderscore}total}
-  although an equation for the replacement of \isa{op\ {\isasymsqsubset}} was only
-  given in the interpretation of \isa{partial{\isacharunderscore}order}.  The
+  The predicate \isa{op\ {\isaliteral{3C}{\isacharless}}} appears in theorem \isa{int{\isaliteral{2E}{\isachardot}}less{\isaliteral{5F}{\isacharunderscore}}total}
+  although an equation for the replacement of \isa{op\ {\isaliteral{5C3C73717375627365743E}{\isasymsqsubset}}} was only
+  given in the interpretation of \isa{partial{\isaliteral{5F}{\isacharunderscore}}order}.  The
   interpretation equations are pushed downwards the hierarchy for
   related interpretations --- that is, for interpretations that share
   the instances of parameters they have in common.
 \end{itemize}%
 \end{isamarkuptext}%

 %
 \begin{isamarkuptext}%
 The interpretations for a locale $n$ within the current
   theory may be inspected with \isakeyword{print\_interps}~$n$.  This
   prints the list of instances of $n$, for which interpretations exist.
-  For example, \isakeyword{print\_interps} \isa{partial{\isacharunderscore}order}
+  For example, \isakeyword{print\_interps} \isa{partial{\isaliteral{5F}{\isacharunderscore}}order}
   outputs the following:
 \begin{small}
 \begin{alltt}
   int! : partial_order "op \(\le\)"
 \end{alltt}

 \isamarkupsection{Locale Expressions \label{sec:expressions}%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-A map~\isa{{\isasymphi}} between partial orders~\isa{{\isasymsqsubseteq}} and~\isa{{\isasympreceq}}
-  is called order preserving if \isa{x\ {\isasymsqsubseteq}\ y} implies \isa{{\isasymphi}\ x\ {\isasympreceq}\ {\isasymphi}\ y}.  This situation is more complex than those encountered so
+A map~\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} between partial orders~\isa{{\isaliteral{5C3C737173756273657465713E}{\isasymsqsubseteq}}} and~\isa{{\isaliteral{5C3C7072656365713E}{\isasympreceq}}}
+  is called order preserving if \isa{x\ {\isaliteral{5C3C737173756273657465713E}{\isasymsqsubseteq}}\ y} implies \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}\ x\ {\isaliteral{5C3C7072656365713E}{\isasympreceq}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\ y}.  This situation is more complex than those encountered so
   far: it involves two partial orders, and it is desirable to use the
   existing locale for both.
 
-  A locale for order preserving maps requires three parameters: \isa{le}~(\isakeyword{infixl}~\isa{{\isasymsqsubseteq}}) and \isa{le{\isacharprime}}~(\isakeyword{infixl}~\isa{{\isasympreceq}}) for the orders and~\isa{{\isasymphi}}
+  A locale for order preserving maps requires three parameters: \isa{le}~(\isakeyword{infixl}~\isa{{\isaliteral{5C3C737173756273657465713E}{\isasymsqsubseteq}}}) and \isa{le{\isaliteral{27}{\isacharprime}}}~(\isakeyword{infixl}~\isa{{\isaliteral{5C3C7072656365713E}{\isasympreceq}}}) for the orders and~\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}}
   for the map.
 
   In order to reuse the existing locale for partial orders, which has
   the single parameter~\isa{le}, it must be imported twice, once
   mapping its parameter to~\isa{le} from the new locale and once
-  to~\isa{le{\isacharprime}}.  This can be achieved with a compound locale
+  to~\isa{le{\isaliteral{27}{\isacharprime}}}.  This can be achieved with a compound locale
   expression.
 
   In general, a locale expression is a sequence of \emph{locale instances}
   separated by~``$\textbf{+}$'' and followed by a \isakeyword{for}
   clause.

   different instances of the same locale.  While in
   \isakeyword{interpretation} qualifiers default to mandatory, in
   import and in the \isakeyword{sublocale} command, they default to
   optional.
 
-  Since the parameters~\isa{le} and~\isa{le{\isacharprime}} are to be partial
+  Since the parameters~\isa{le} and~\isa{le{\isaliteral{27}{\isacharprime}}} are to be partial
   orders, our locale for order preserving maps will import the these
   instances:
 \begin{small}
 \begin{alltt}
   le: partial_order le

   only occur after the import section, and therefore the parameters
   referred to in the instances must be declared in the \isakeyword{for}
   clause.  The \isakeyword{for} clause is also where the syntax of these
   parameters is declared.
 
-  Two context elements for the map parameter~\isa{{\isasymphi}} and the
+  Two context elements for the map parameter~\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} and the
   assumptions that it is order preserving complete the locale
   declaration.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \ \ \isacommand{locale}\isamarkupfalse%
-\ order{\isacharunderscore}preserving\ {\isacharequal}\isanewline
-\ \ \ \ le{\isacharcolon}\ partial{\isacharunderscore}order\ le\ {\isacharplus}\ le{\isacharprime}{\isacharcolon}\ partial{\isacharunderscore}order\ le{\isacharprime}\isanewline
-\ \ \ \ \ \ \isakeyword{for}\ le\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqsubseteq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{and}\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline
-\ \ \ \ \isakeyword{fixes}\ {\isasymphi}\isanewline
-\ \ \ \ \isakeyword{assumes}\ hom{\isacharunderscore}le{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymsqsubseteq}\ y\ {\isasymLongrightarrow}\ {\isasymphi}\ x\ {\isasympreceq}\ {\isasymphi}\ y{\isachardoublequoteclose}%
+\ order{\isaliteral{5F}{\isacharunderscore}}preserving\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ \ \ le{\isaliteral{3A}{\isacharcolon}}\ partial{\isaliteral{5F}{\isacharunderscore}}order\ le\ {\isaliteral{2B}{\isacharplus}}\ le{\isaliteral{27}{\isacharprime}}{\isaliteral{3A}{\isacharcolon}}\ partial{\isaliteral{5F}{\isacharunderscore}}order\ le{\isaliteral{27}{\isacharprime}}\isanewline
+\ \ \ \ \ \ \isakeyword{for}\ le\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C737173756273657465713E}{\isasymsqsubseteq}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{5}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ \isakeyword{and}\ le{\isaliteral{27}{\isacharprime}}\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C7072656365713E}{\isasympreceq}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{5}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\isanewline
+\ \ \ \ \isakeyword{fixes}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isanewline
+\ \ \ \ \isakeyword{assumes}\ hom{\isaliteral{5F}{\isacharunderscore}}le{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C737173756273657465713E}{\isasymsqsubseteq}}\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\ x\ {\isaliteral{5C3C7072656365713E}{\isasympreceq}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\ y{\isaliteral{22}{\isachardoublequoteclose}}%
 \begin{isamarkuptext}%
 Here are examples of theorems that are
   available in the locale:
 
-  \hspace*{1em}\isa{hom{\isacharunderscore}le}: \isa{{\isacharquery}x\ {\isasymsqsubseteq}\ {\isacharquery}y\ {\isasymLongrightarrow}\ {\isasymphi}\ {\isacharquery}x\ {\isasympreceq}\ {\isasymphi}\ {\isacharquery}y}
-
-  \hspace*{1em}\isa{le{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: \isa{{\isasymlbrakk}{\isacharquery}x\ {\isasymsqsubset}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasymsqsubseteq}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymsqsubset}\ {\isacharquery}z}
-
-  \hspace*{1em}\isa{le{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}:
+  \hspace*{1em}\isa{hom{\isaliteral{5F}{\isacharunderscore}}le}: \isa{{\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C737173756273657465713E}{\isasymsqsubseteq}}\ {\isaliteral{3F}{\isacharquery}}y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C7072656365713E}{\isasympreceq}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\ {\isaliteral{3F}{\isacharquery}}y}
+
+  \hspace*{1em}\isa{le{\isaliteral{2E}{\isachardot}}less{\isaliteral{5F}{\isacharunderscore}}le{\isaliteral{5F}{\isacharunderscore}}trans}: \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C73717375627365743E}{\isasymsqsubset}}\ {\isaliteral{3F}{\isacharquery}}y{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{3F}{\isacharquery}}y\ {\isaliteral{5C3C737173756273657465713E}{\isasymsqsubseteq}}\ {\isaliteral{3F}{\isacharquery}}z{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C73717375627365743E}{\isasymsqsubset}}\ {\isaliteral{3F}{\isacharquery}}z}
+
+  \hspace*{1em}\isa{le{\isaliteral{27}{\isacharprime}}{\isaliteral{2E}{\isachardot}}less{\isaliteral{5F}{\isacharunderscore}}le{\isaliteral{5F}{\isacharunderscore}}trans}:
   \begin{isabelle}%
-\ \ \ \ {\isasymlbrakk}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasympreceq}\ {\isacharquery}x\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\isanewline
-\isaindent{\ \ \ \ }{\isasymLongrightarrow}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasympreceq}\ {\isacharquery}x\ {\isacharquery}z%
+\ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}partial{\isaliteral{5F}{\isacharunderscore}}order{\isaliteral{2E}{\isachardot}}less\ op\ {\isaliteral{5C3C7072656365713E}{\isasympreceq}}\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{3F}{\isacharquery}}y{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{3F}{\isacharquery}}y\ {\isaliteral{5C3C7072656365713E}{\isasympreceq}}\ {\isaliteral{3F}{\isacharquery}}z{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline
+\isaindent{\ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ partial{\isaliteral{5F}{\isacharunderscore}}order{\isaliteral{2E}{\isachardot}}less\ op\ {\isaliteral{5C3C7072656365713E}{\isasympreceq}}\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{3F}{\isacharquery}}z%
 \end{isabelle}
   While there is infix syntax for the strict operation associated to
-  \isa{op\ {\isasymsqsubseteq}}, there is none for the strict version of \isa{op\ {\isasympreceq}}.  The abbreviation \isa{less} with its infix syntax is only
+  \isa{op\ {\isaliteral{5C3C737173756273657465713E}{\isasymsqsubseteq}}}, there is none for the strict version of \isa{op\ {\isaliteral{5C3C7072656365713E}{\isasympreceq}}}.  The abbreviation \isa{less} with its infix syntax is only
   available for the original instance it was declared for.  We may
-  introduce the abbreviation \isa{less{\isacharprime}} with infix syntax~\isa{{\isasymprec}}
+  introduce the abbreviation \isa{less{\isaliteral{27}{\isacharprime}}} with infix syntax~\isa{{\isaliteral{5C3C707265633E}{\isasymprec}}}
   with the following declaration:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \ \ \isacommand{abbreviation}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{in}\ order{\isacharunderscore}preserving{\isacharparenright}\isanewline
-\ \ \ \ less{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymprec}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}less{\isacharprime}\ {\isasymequiv}\ partial{\isacharunderscore}order{\isachardot}less\ le{\isacharprime}{\isachardoublequoteclose}%
+\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{in}\ order{\isaliteral{5F}{\isacharunderscore}}preserving{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ less{\isaliteral{27}{\isacharprime}}\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C707265633E}{\isasymprec}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{5}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}less{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ partial{\isaliteral{5F}{\isacharunderscore}}order{\isaliteral{2E}{\isachardot}}less\ le{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequoteclose}}%
 \begin{isamarkuptext}%
 Now the theorem is displayed nicely as
-  \isa{le{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}:
+  \isa{le{\isaliteral{27}{\isacharprime}}{\isaliteral{2E}{\isachardot}}less{\isaliteral{5F}{\isacharunderscore}}le{\isaliteral{5F}{\isacharunderscore}}trans}:
   \begin{isabelle}%
-\ \ {\isasymlbrakk}{\isacharquery}x\ {\isasymprec}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymprec}\ {\isacharquery}z%
+\ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C707265633E}{\isasymprec}}\ {\isaliteral{3F}{\isacharquery}}y{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{3F}{\isacharquery}}y\ {\isaliteral{5C3C7072656365713E}{\isasympreceq}}\ {\isaliteral{3F}{\isacharquery}}z{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C707265633E}{\isasymprec}}\ {\isaliteral{3F}{\isacharquery}}z%
 \end{isabelle}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%

 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
 It is possible to omit parameter instantiations.  The
   instantiation then defaults to the name of
-  the parameter itself.  For example, the locale expression \isa{partial{\isacharunderscore}order} is short for \isa{partial{\isacharunderscore}order\ le}, since the
+  the parameter itself.  For example, the locale expression \isa{partial{\isaliteral{5F}{\isacharunderscore}}order} is short for \isa{partial{\isaliteral{5F}{\isacharunderscore}}order\ le}, since the
   locale's single parameter is~\isa{le}.  We took advantage of this
   in the \isakeyword{sublocale} declarations of
   Section~\ref{sec:changing-the-hierarchy}.%
 \end{isamarkuptext}%
 \isamarkuptrue%

   There is an exception to this rule in locale declarations, where the
   \isakeyword{for} clause serves to declare locale parameters.  Here,
   locale parameters for which no parameter instantiation is given are
   implicitly added, with their mixfix syntax, at the beginning of the
   \isakeyword{for} clause.  For example, in a locale declaration, the
-  expression \isa{partial{\isacharunderscore}order} is short for
+  expression \isa{partial{\isaliteral{5F}{\isacharunderscore}}order} is short for
 \begin{small}
 \begin{alltt}
   partial_order le \isakeyword{for} le (\isakeyword{infixl} "\(\sqsubseteq\)" 50)\textrm{.}
 \end{alltt}
 \end{small}

 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
 The following locale declarations provide more examples.  A
-  map~\isa{{\isasymphi}} is a lattice homomorphism if it preserves meet and
+  map~\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} is a lattice homomorphism if it preserves meet and
   join.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \ \ \isacommand{locale}\isamarkupfalse%
-\ lattice{\isacharunderscore}hom\ {\isacharequal}\isanewline
-\ \ \ \ le{\isacharcolon}\ lattice\ {\isacharplus}\ le{\isacharprime}{\isacharcolon}\ lattice\ le{\isacharprime}\ \isakeyword{for}\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline
-\ \ \ \ \isakeyword{fixes}\ {\isasymphi}\isanewline
-\ \ \ \ \isakeyword{assumes}\ hom{\isacharunderscore}meet{\isacharcolon}\ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}x\ {\isasymsqinter}\ y{\isacharparenright}\ {\isacharequal}\ le{\isacharprime}{\isachardot}meet\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \isakeyword{and}\ hom{\isacharunderscore}join{\isacharcolon}\ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}x\ {\isasymsqunion}\ y{\isacharparenright}\ {\isacharequal}\ le{\isacharprime}{\isachardot}join\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}%
+\ lattice{\isaliteral{5F}{\isacharunderscore}}hom\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ \ \ le{\isaliteral{3A}{\isacharcolon}}\ lattice\ {\isaliteral{2B}{\isacharplus}}\ le{\isaliteral{27}{\isacharprime}}{\isaliteral{3A}{\isacharcolon}}\ lattice\ le{\isaliteral{27}{\isacharprime}}\ \isakeyword{for}\ le{\isaliteral{27}{\isacharprime}}\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C7072656365713E}{\isasympreceq}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{5}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\isanewline
+\ \ \ \ \isakeyword{fixes}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isanewline
+\ \ \ \ \isakeyword{assumes}\ hom{\isaliteral{5F}{\isacharunderscore}}meet{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C7068693E}{\isasymphi}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C7371696E7465723E}{\isasymsqinter}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ le{\isaliteral{27}{\isacharprime}}{\isaliteral{2E}{\isachardot}}meet\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7068693E}{\isasymphi}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7068693E}{\isasymphi}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \ \ \ \ \isakeyword{and}\ hom{\isaliteral{5F}{\isacharunderscore}}join{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C7068693E}{\isasymphi}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C7371756E696F6E3E}{\isasymsqunion}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ le{\isaliteral{27}{\isacharprime}}{\isaliteral{2E}{\isachardot}}join\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7068693E}{\isasymphi}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7068693E}{\isasymphi}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
 \begin{isamarkuptext}%
 The parameter instantiation in the first instance of \isa{lattice} is omitted.  This causes the parameter~\isa{le} to be
   added to the \isakeyword{for} clause, and the locale has
-  parameters~\isa{le},~\isa{le{\isacharprime}} and, of course,~\isa{{\isasymphi}}.
+  parameters~\isa{le},~\isa{le{\isaliteral{27}{\isacharprime}}} and, of course,~\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}}.
 
   Before turning to the second example, we complete the locale by
   providing infix syntax for the meet and join operations of the
   second lattice.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \ \ \isacommand{context}\isamarkupfalse%
-\ lattice{\isacharunderscore}hom\ \isakeyword{begin}\isanewline
+\ lattice{\isaliteral{5F}{\isacharunderscore}}hom\ \isakeyword{begin}\isanewline
 \ \ \isacommand{abbreviation}\isamarkupfalse%
-\ meet{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqinter}{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}meet{\isacharprime}\ {\isasymequiv}\ le{\isacharprime}{\isachardot}meet{\isachardoublequoteclose}\isanewline
+\ meet{\isaliteral{27}{\isacharprime}}\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C7371696E7465723E}{\isasymsqinter}}{\isaliteral{27}{\isacharprime}}{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{5}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}meet{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ le{\isaliteral{27}{\isacharprime}}{\isaliteral{2E}{\isachardot}}meet{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \ \ \isacommand{abbreviation}\isamarkupfalse%
-\ join{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqunion}{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}join{\isacharprime}\ {\isasymequiv}\ le{\isacharprime}{\isachardot}join{\isachardoublequoteclose}\isanewline
+\ join{\isaliteral{27}{\isacharprime}}\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C7371756E696F6E3E}{\isasymsqunion}}{\isaliteral{27}{\isacharprime}}{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{5}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}join{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ le{\isaliteral{27}{\isacharprime}}{\isaliteral{2E}{\isachardot}}join{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \ \ \isacommand{end}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 The next example makes radical use of the short hand
   facilities.  A homomorphism is an endomorphism if both orders
   coincide.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \ \ \isacommand{locale}\isamarkupfalse%
-\ lattice{\isacharunderscore}end\ {\isacharequal}\ lattice{\isacharunderscore}hom\ {\isacharunderscore}\ le%
-\begin{isamarkuptext}%
-The notation~\isa{{\isacharunderscore}} enables to omit a parameter in a
+\ lattice{\isaliteral{5F}{\isacharunderscore}}end\ {\isaliteral{3D}{\isacharequal}}\ lattice{\isaliteral{5F}{\isacharunderscore}}hom\ {\isaliteral{5F}{\isacharunderscore}}\ le%
+\begin{isamarkuptext}%
+The notation~\isa{{\isaliteral{5F}{\isacharunderscore}}} enables to omit a parameter in a
   positional instantiation.  The omitted parameter,~\isa{le} becomes
   the parameter of the declared locale and is, in the following
-  position, used to instantiate the second parameter of \isa{lattice{\isacharunderscore}hom}.  The effect is that of identifying the first in second
+  position, used to instantiate the second parameter of \isa{lattice{\isaliteral{5F}{\isacharunderscore}}hom}.  The effect is that of identifying the first in second
   parameter of the homomorphism locale.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
 The inheritance diagram of the situation we have now is shown
   in Figure~\ref{fig:hom}, where the dashed line depicts an
   interpretation which is introduced below.  Parameter instantiations
   are indicated by $\sqsubseteq \mapsto \preceq$ etc.  By looking at
   the inheritance diagram it would seem
-  that two identical copies of each of the locales \isa{partial{\isacharunderscore}order} and \isa{lattice} are imported by \isa{lattice{\isacharunderscore}end}.  This is not the case!  Inheritance paths with
+  that two identical copies of each of the locales \isa{partial{\isaliteral{5F}{\isacharunderscore}}order} and \isa{lattice} are imported by \isa{lattice{\isaliteral{5F}{\isacharunderscore}}end}.  This is not the case!  Inheritance paths with
   identical morphisms are automatically detected and
   the conclusions of the respective locales appear only once.
 
 \begin{figure}
 \hrule \vspace{2ex}
 \begin{center}
 \begin{tikzpicture}
-  \node (o) at (0,0) {\isa{partial{\isacharunderscore}order}};
-  \node (oh) at (1.5,-2) {\isa{order{\isacharunderscore}preserving}};
+  \node (o) at (0,0) {\isa{partial{\isaliteral{5F}{\isacharunderscore}}order}};
+  \node (oh) at (1.5,-2) {\isa{order{\isaliteral{5F}{\isacharunderscore}}preserving}};
   \node (oh1) at (1.5,-0.7) {$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$};
   \node (oh2) at (0,-1.3) {$\scriptscriptstyle \sqsubseteq \mapsto \preceq$};
   \node (l) at (-1.5,-2) {\isa{lattice}};
-  \node (lh) at (0,-4) {\isa{lattice{\isacharunderscore}hom}};
+  \node (lh) at (0,-4) {\isa{lattice{\isaliteral{5F}{\isacharunderscore}}hom}};
   \node (lh1) at (0,-2.7) {$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$};
   \node (lh2) at (-1.5,-3.3) {$\scriptscriptstyle \sqsubseteq \mapsto \preceq$};
-  \node (le) at (0,-6) {\isa{lattice{\isacharunderscore}end}};
+  \node (le) at (0,-6) {\isa{lattice{\isaliteral{5F}{\isacharunderscore}}end}};
   \node (le1) at (0,-4.8)
     [anchor=west]{$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$};
   \node (le2) at (0,-5.2)
     [anchor=west]{$\scriptscriptstyle \preceq \mapsto \sqsubseteq$};
   \draw (o) -- (l);

   preserving.  As the final example of this section, a locale
   interpretation is used to assert this:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \ \ \isacommand{sublocale}\isamarkupfalse%
-\ lattice{\isacharunderscore}hom\ {\isasymsubseteq}\ order{\isacharunderscore}preserving%
+\ lattice{\isaliteral{5F}{\isacharunderscore}}hom\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ order{\isaliteral{5F}{\isacharunderscore}}preserving%
 \isadelimproof
 \ %
 \endisadelimproof
 %
 \isatagproof
 \isacommand{proof}\isamarkupfalse%
-\ unfold{\isacharunderscore}locales\isanewline
+\ unfold{\isaliteral{5F}{\isacharunderscore}}locales\isanewline
 \ \ \ \ \isacommand{fix}\isamarkupfalse%
 \ x\ y\isanewline
 \ \ \ \ \isacommand{assume}\isamarkupfalse%
-\ {\isachardoublequoteopen}x\ {\isasymsqsubseteq}\ y{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C737173756273657465713E}{\isasymsqsubseteq}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \ \ \ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}y\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymsqunion}\ y{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ add{\isacharcolon}\ le{\isachardot}join{\isacharunderscore}connection{\isacharparenright}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C7371756E696F6E3E}{\isasymsqunion}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ le{\isaliteral{2E}{\isachardot}}join{\isaliteral{5F}{\isacharunderscore}}connection{\isaliteral{29}{\isacharparenright}}\isanewline
 \ \ \ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymphi}\ y\ {\isacharequal}\ {\isacharparenleft}{\isasymphi}\ x\ {\isasymsqunion}{\isacharprime}\ {\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ add{\isacharcolon}\ hom{\isacharunderscore}join\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C7068693E}{\isasymphi}}\ y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7068693E}{\isasymphi}}\ x\ {\isaliteral{5C3C7371756E696F6E3E}{\isasymsqunion}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ hom{\isaliteral{5F}{\isacharunderscore}}join\ {\isaliteral{5B}{\isacharbrackleft}}symmetric{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline
 \ \ \ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymphi}\ x\ {\isasympreceq}\ {\isasymphi}\ y{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ add{\isacharcolon}\ le{\isacharprime}{\isachardot}join{\isacharunderscore}connection{\isacharparenright}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C7068693E}{\isasymphi}}\ x\ {\isaliteral{5C3C7072656365713E}{\isasympreceq}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ le{\isaliteral{27}{\isacharprime}}{\isaliteral{2E}{\isachardot}}join{\isaliteral{5F}{\isacharunderscore}}connection{\isaliteral{29}{\isacharparenright}}\isanewline
 \ \ \isacommand{qed}\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
 %

 %
 \endisadelimproof
 %
 \begin{isamarkuptext}%
 Theorems and other declarations --- syntax, in particular --- from
-  the locale \isa{order{\isacharunderscore}preserving} are now active in \isa{lattice{\isacharunderscore}hom}, for example
-  \isa{hom{\isacharunderscore}le}:
+  the locale \isa{order{\isaliteral{5F}{\isacharunderscore}}preserving} are now active in \isa{lattice{\isaliteral{5F}{\isacharunderscore}}hom}, for example
+  \isa{hom{\isaliteral{5F}{\isacharunderscore}}le}:
   \begin{isabelle}%
-\ \ {\isacharquery}x\ {\isasymsqsubseteq}\ {\isacharquery}y\ {\isasymLongrightarrow}\ {\isasymphi}\ {\isacharquery}x\ {\isasympreceq}\ {\isasymphi}\ {\isacharquery}y%
+\ \ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C737173756273657465713E}{\isasymsqsubseteq}}\ {\isaliteral{3F}{\isacharquery}}y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C7072656365713E}{\isasympreceq}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\ {\isaliteral{3F}{\isacharquery}}y%
 \end{isabelle}
   This theorem will be useful in the following section.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %

 %
 \begin{isamarkuptext}%
 There are situations where an interpretation is not possible
   in the general case since the desired property is only valid if
   certain conditions are fulfilled.  Take, for example, the function
-  \isa{{\isasymlambda}i{\isachardot}\ n\ {\isacharasterisk}\ i} that scales its argument by a constant factor.
+  \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}i{\isaliteral{2E}{\isachardot}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ i} that scales its argument by a constant factor.
   This function is order preserving (and even a lattice endomorphism)
-  with respect to \isa{op\ {\isasymle}} provided \isa{n\ {\isasymge}\ {\isadigit{0}}}.
+  with respect to \isa{op\ {\isaliteral{5C3C6C653E}{\isasymle}}} provided \isa{n\ {\isaliteral{5C3C67653E}{\isasymge}}\ {\isadigit{0}}}.
 
   It is not possible to express this using a global interpretation,
   because it is in general unspecified whether~\isa{n} is
   non-negative, but one may make an interpretation in an inner context
   of a proof where full information is available.

   this can be done with the \isakeyword{sublocale} command.  For this
   purpose, we introduce a locale for the condition.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \ \ \isacommand{locale}\isamarkupfalse%
-\ non{\isacharunderscore}negative\ {\isacharequal}\isanewline
-\ \ \ \ \isakeyword{fixes}\ n\ {\isacharcolon}{\isacharcolon}\ int\isanewline
-\ \ \ \ \isakeyword{assumes}\ non{\isacharunderscore}neg{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymle}\ n{\isachardoublequoteclose}%
+\ non{\isaliteral{5F}{\isacharunderscore}}negative\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ \ \ \isakeyword{fixes}\ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\isanewline
+\ \ \ \ \isakeyword{assumes}\ non{\isaliteral{5F}{\isacharunderscore}}neg{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isadigit{0}}\ {\isaliteral{5C3C6C653E}{\isasymle}}\ n{\isaliteral{22}{\isachardoublequoteclose}}%
 \begin{isamarkuptext}%
 It is again convenient to make the interpretation in an
   incremental fashion, first for order preserving maps, the for
   lattice endomorphisms.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \ \ \isacommand{sublocale}\isamarkupfalse%
-\ non{\isacharunderscore}negative\ {\isasymsubseteq}\isanewline
-\ \ \ \ \ \ order{\isacharunderscore}preserving\ {\isachardoublequoteopen}op\ {\isasymle}{\isachardoublequoteclose}\ {\isachardoublequoteopen}op\ {\isasymle}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymlambda}i{\isachardot}\ n\ {\isacharasterisk}\ i{\isachardoublequoteclose}\isanewline
+\ non{\isaliteral{5F}{\isacharunderscore}}negative\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\isanewline
+\ \ \ \ \ \ order{\isaliteral{5F}{\isacharunderscore}}preserving\ {\isaliteral{22}{\isachardoublequoteopen}}op\ {\isaliteral{5C3C6C653E}{\isasymle}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}op\ {\isaliteral{5C3C6C653E}{\isasymle}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}i{\isaliteral{2E}{\isachardot}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ i{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 %
 \isadelimproof
 \ \ \ \ %
 \endisadelimproof
 %
 \isatagproof
 \isacommand{using}\isamarkupfalse%
-\ non{\isacharunderscore}neg\ \isacommand{by}\isamarkupfalse%
-\ unfold{\isacharunderscore}locales\ {\isacharparenleft}rule\ mult{\isacharunderscore}left{\isacharunderscore}mono{\isacharparenright}%
+\ non{\isaliteral{5F}{\isacharunderscore}}neg\ \isacommand{by}\isamarkupfalse%
+\ unfold{\isaliteral{5F}{\isacharunderscore}}locales\ {\isaliteral{28}{\isacharparenleft}}rule\ mult{\isaliteral{5F}{\isacharunderscore}}left{\isaliteral{5F}{\isacharunderscore}}mono{\isaliteral{29}{\isacharparenright}}%
 \endisatagproof
 {\isafoldproof}%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \begin{isamarkuptext}%
 While the proof of the previous interpretation
-  is straightforward from monotonicity lemmas for~\isa{op\ {\isacharasterisk}}, the
+  is straightforward from monotonicity lemmas for~\isa{op\ {\isaliteral{2A}{\isacharasterisk}}}, the
   second proof follows a useful pattern.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isadelimvisible
 \ \ %
 \endisadelimvisible
 %
 \isatagvisible
 \isacommand{sublocale}\isamarkupfalse%
-\ non{\isacharunderscore}negative\ {\isasymsubseteq}\ lattice{\isacharunderscore}end\ {\isachardoublequoteopen}op\ {\isasymle}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymlambda}i{\isachardot}\ n\ {\isacharasterisk}\ i{\isachardoublequoteclose}\isanewline
+\ non{\isaliteral{5F}{\isacharunderscore}}negative\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ lattice{\isaliteral{5F}{\isacharunderscore}}end\ {\isaliteral{22}{\isachardoublequoteopen}}op\ {\isaliteral{5C3C6C653E}{\isasymle}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}i{\isaliteral{2E}{\isachardot}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ i{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \ \ \isacommand{proof}\isamarkupfalse%
-\ {\isacharparenleft}unfold{\isacharunderscore}locales{\isacharcomma}\ unfold\ int{\isacharunderscore}min{\isacharunderscore}eq\ int{\isacharunderscore}max{\isacharunderscore}eq{\isacharparenright}%
+\ {\isaliteral{28}{\isacharparenleft}}unfold{\isaliteral{5F}{\isacharunderscore}}locales{\isaliteral{2C}{\isacharcomma}}\ unfold\ int{\isaliteral{5F}{\isacharunderscore}}min{\isaliteral{5F}{\isacharunderscore}}eq\ int{\isaliteral{5F}{\isacharunderscore}}max{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{29}{\isacharparenright}}%
 \begin{isamarkuptxt}%
 \normalsize Unfolding the locale predicates \emph{and} the
       interpretation equations immediately yields two subgoals that
       reflect the core conjecture.
       \begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ n\ {\isacharasterisk}\ min\ x\ y\ {\isacharequal}\ min\ {\isacharparenleft}n\ {\isacharasterisk}\ x{\isacharparenright}\ {\isacharparenleft}n\ {\isacharasterisk}\ y{\isacharparenright}\isanewline
-\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ n\ {\isacharasterisk}\ max\ x\ y\ {\isacharequal}\ max\ {\isacharparenleft}n\ {\isacharasterisk}\ x{\isacharparenright}\ {\isacharparenleft}n\ {\isacharasterisk}\ y{\isacharparenright}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y{\isaliteral{2E}{\isachardot}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ min\ x\ y\ {\isaliteral{3D}{\isacharequal}}\ min\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2A}{\isacharasterisk}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2A}{\isacharasterisk}}\ y{\isaliteral{29}{\isacharparenright}}\isanewline
+\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y{\isaliteral{2E}{\isachardot}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ max\ x\ y\ {\isaliteral{3D}{\isacharequal}}\ max\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2A}{\isacharasterisk}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2A}{\isacharasterisk}}\ y{\isaliteral{29}{\isacharparenright}}%
 \end{isabelle}
-      It is now necessary to show, in the context of \isa{non{\isacharunderscore}negative}, that multiplication by~\isa{n} commutes with
+      It is now necessary to show, in the context of \isa{non{\isaliteral{5F}{\isacharunderscore}}negative}, that multiplication by~\isa{n} commutes with
       \isa{min} and \isa{max}.%
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \ \ \isacommand{qed}\isamarkupfalse%
-\ {\isacharparenleft}auto\ simp{\isacharcolon}\ hom{\isacharunderscore}le{\isacharparenright}%
+\ {\isaliteral{28}{\isacharparenleft}}auto\ simp{\isaliteral{3A}{\isacharcolon}}\ hom{\isaliteral{5F}{\isacharunderscore}}le{\isaliteral{29}{\isacharparenright}}%
 \endisatagvisible
 {\isafoldvisible}%
 %
 \isadelimvisible
 %
 \endisadelimvisible
 %
 \begin{isamarkuptext}%
-The lemma \isa{hom{\isacharunderscore}le}
+The lemma \isa{hom{\isaliteral{5F}{\isacharunderscore}}le}
   simplifies a proof that would have otherwise been lengthy and we may
   consider making it a default rule for the simplifier:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \ \ \isacommand{lemmas}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{in}\ order{\isacharunderscore}preserving{\isacharparenright}\ hom{\isacharunderscore}le\ {\isacharbrackleft}simp{\isacharbrackright}%
+\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{in}\ order{\isaliteral{5F}{\isacharunderscore}}preserving{\isaliteral{29}{\isacharparenright}}\ hom{\isaliteral{5F}{\isacharunderscore}}le\ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}%
 \isamarkupsubsection{Avoiding Infinite Chains of Interpretations
   \label{sec:infinite-chains}%
 }
 \isamarkuptrue%
 %

 \ \ %
 \endisadelimvisible
 %
 \isatagvisible
 \isacommand{sublocale}\isamarkupfalse%
-\ partial{\isacharunderscore}order\ {\isasymsubseteq}\ f{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}{\isasymlambda}f\ g{\isachardot}\ {\isasymforall}x{\isachardot}\ f\ x\ {\isasymsqsubseteq}\ g\ x{\isachardoublequoteclose}\isanewline
+\ partial{\isaliteral{5F}{\isacharunderscore}}order\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ f{\isaliteral{3A}{\isacharcolon}}\ partial{\isaliteral{5F}{\isacharunderscore}}order\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}f\ g{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ f\ x\ {\isaliteral{5C3C737173756273657465713E}{\isasymsqsubseteq}}\ g\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \ \ \ \ \isacommand{oops}\isamarkupfalse%
 %
 \endisatagvisible
 {\isafoldvisible}%
 %

 %
 \begin{isamarkuptext}%
 Unfortunately this is a cyclic interpretation that leads to an
   infinite chain, namely
   \begin{isabelle}%
-\ \ partial{\isacharunderscore}order\ {\isasymsubseteq}\ partial{\isacharunderscore}order\ {\isacharparenleft}{\isasymlambda}f\ g{\isachardot}\ {\isasymforall}x{\isachardot}\ f\ x\ {\isasymsqsubseteq}\ g\ x{\isacharparenright}\ {\isasymsubseteq}\isanewline
-\isaindent{\ \ }\ \ partial{\isacharunderscore}order\ {\isacharparenleft}{\isasymlambda}f\ g{\isachardot}\ {\isasymforall}x\ y{\isachardot}\ f\ x\ y\ {\isasymsqsubseteq}\ g\ x\ y{\isacharparenright}\ {\isasymsubseteq}\ \ {\isasymdots}%
+\ \ partial{\isaliteral{5F}{\isacharunderscore}}order\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ partial{\isaliteral{5F}{\isacharunderscore}}order\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}f\ g{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ f\ x\ {\isaliteral{5C3C737173756273657465713E}{\isasymsqsubseteq}}\ g\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\isanewline
+\isaindent{\ \ }\ \ partial{\isaliteral{5F}{\isacharunderscore}}order\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}f\ g{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x\ y{\isaliteral{2E}{\isachardot}}\ f\ x\ y\ {\isaliteral{5C3C737173756273657465713E}{\isasymsqsubseteq}}\ g\ x\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ \ {\isaliteral{5C3C646F74733E}{\isasymdots}}%
 \end{isabelle}
   and the interpretation is rejected.
 
   Instead it is necessary to declare a locale that is logically
-  equivalent to \isa{partial{\isacharunderscore}order} but serves to collect facts
+  equivalent to \isa{partial{\isaliteral{5F}{\isacharunderscore}}order} but serves to collect facts
   about functions spaces where the co-domain is a partial order, and
   to make the interpretation in its context:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \ \ \isacommand{locale}\isamarkupfalse%
-\ fun{\isacharunderscore}partial{\isacharunderscore}order\ {\isacharequal}\ partial{\isacharunderscore}order\isanewline
+\ fun{\isaliteral{5F}{\isacharunderscore}}partial{\isaliteral{5F}{\isacharunderscore}}order\ {\isaliteral{3D}{\isacharequal}}\ partial{\isaliteral{5F}{\isacharunderscore}}order\isanewline
 \isanewline
 \ \ \isacommand{sublocale}\isamarkupfalse%
-\ fun{\isacharunderscore}partial{\isacharunderscore}order\ {\isasymsubseteq}\isanewline
-\ \ \ \ \ \ f{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}{\isasymlambda}f\ g{\isachardot}\ {\isasymforall}x{\isachardot}\ f\ x\ {\isasymsqsubseteq}\ g\ x{\isachardoublequoteclose}\isanewline
+\ fun{\isaliteral{5F}{\isacharunderscore}}partial{\isaliteral{5F}{\isacharunderscore}}order\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\isanewline
+\ \ \ \ \ \ f{\isaliteral{3A}{\isacharcolon}}\ partial{\isaliteral{5F}{\isacharunderscore}}order\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}f\ g{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ f\ x\ {\isaliteral{5C3C737173756273657465713E}{\isasymsqsubseteq}}\ g\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 %
 \isadelimproof
 \ \ \ \ %
 \endisadelimproof
 %
 \isatagproof
 \isacommand{by}\isamarkupfalse%
-\ unfold{\isacharunderscore}locales\ {\isacharparenleft}fast{\isacharcomma}rule{\isacharcomma}fast{\isacharcomma}blast\ intro{\isacharcolon}\ trans{\isacharparenright}%
+\ unfold{\isaliteral{5F}{\isacharunderscore}}locales\ {\isaliteral{28}{\isacharparenleft}}fast{\isaliteral{2C}{\isacharcomma}}rule{\isaliteral{2C}{\isacharcomma}}fast{\isaliteral{2C}{\isacharcomma}}blast\ intro{\isaliteral{3A}{\isacharcolon}}\ trans{\isaliteral{29}{\isacharparenright}}%
 \endisatagproof
 {\isafoldproof}%
 %
 \isadelimproof
 %

   related hierarchy.  By means of the same lifting, a function space
   is a lattice if its co-domain is a lattice:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \ \ \isacommand{locale}\isamarkupfalse%
-\ fun{\isacharunderscore}lattice\ {\isacharequal}\ fun{\isacharunderscore}partial{\isacharunderscore}order\ {\isacharplus}\ lattice\isanewline
+\ fun{\isaliteral{5F}{\isacharunderscore}}lattice\ {\isaliteral{3D}{\isacharequal}}\ fun{\isaliteral{5F}{\isacharunderscore}}partial{\isaliteral{5F}{\isacharunderscore}}order\ {\isaliteral{2B}{\isacharplus}}\ lattice\isanewline
 \isanewline
 \ \ \isacommand{sublocale}\isamarkupfalse%
-\ fun{\isacharunderscore}lattice\ {\isasymsubseteq}\ f{\isacharcolon}\ lattice\ {\isachardoublequoteopen}{\isasymlambda}f\ g{\isachardot}\ {\isasymforall}x{\isachardot}\ f\ x\ {\isasymsqsubseteq}\ g\ x{\isachardoublequoteclose}\isanewline
+\ fun{\isaliteral{5F}{\isacharunderscore}}lattice\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ f{\isaliteral{3A}{\isacharcolon}}\ lattice\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}f\ g{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ f\ x\ {\isaliteral{5C3C737173756273657465713E}{\isasymsqsubseteq}}\ g\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 %
 \isadelimproof
 \ \ \ \ %
 \endisadelimproof
 %
 \isatagproof
 \isacommand{proof}\isamarkupfalse%
-\ unfold{\isacharunderscore}locales\isanewline
+\ unfold{\isaliteral{5F}{\isacharunderscore}}locales\isanewline
 \ \ \ \ \isacommand{fix}\isamarkupfalse%
 \ f\ g\isanewline
 \ \ \ \ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}is{\isacharunderscore}inf\ {\isacharparenleft}{\isasymlambda}f\ g{\isachardot}\ {\isasymforall}x{\isachardot}\ f\ x\ {\isasymsqsubseteq}\ g\ x{\isacharparenright}\ f\ g\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ f\ x\ {\isasymsqinter}\ g\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}partial{\isaliteral{5F}{\isacharunderscore}}order{\isaliteral{2E}{\isachardot}}is{\isaliteral{5F}{\isacharunderscore}}inf\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}f\ g{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ f\ x\ {\isaliteral{5C3C737173756273657465713E}{\isasymsqsubseteq}}\ g\ x{\isaliteral{29}{\isacharparenright}}\ f\ g\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ f\ x\ {\isaliteral{5C3C7371696E7465723E}{\isasymsqinter}}\ g\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}rule\ is{\isacharunderscore}infI{\isacharparenright}\ \isacommand{apply}\isamarkupfalse%
-\ rule{\isacharplus}\ \isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}drule\ spec{\isacharcomma}\ assumption{\isacharparenright}{\isacharplus}\ \isacommand{done}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}rule\ is{\isaliteral{5F}{\isacharunderscore}}infI{\isaliteral{29}{\isacharparenright}}\ \isacommand{apply}\isamarkupfalse%
+\ rule{\isaliteral{2B}{\isacharplus}}\ \isacommand{apply}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}drule\ spec{\isaliteral{2C}{\isacharcomma}}\ assumption{\isaliteral{29}{\isacharparenright}}{\isaliteral{2B}{\isacharplus}}\ \isacommand{done}\isamarkupfalse%
 \isanewline
 \ \ \ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymexists}inf{\isachardot}\ partial{\isacharunderscore}order{\isachardot}is{\isacharunderscore}inf\ {\isacharparenleft}{\isasymlambda}f\ g{\isachardot}\ {\isasymforall}x{\isachardot}\ f\ x\ {\isasymsqsubseteq}\ g\ x{\isacharparenright}\ f\ g\ inf{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}inf{\isaliteral{2E}{\isachardot}}\ partial{\isaliteral{5F}{\isacharunderscore}}order{\isaliteral{2E}{\isachardot}}is{\isaliteral{5F}{\isacharunderscore}}inf\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}f\ g{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ f\ x\ {\isaliteral{5C3C737173756273657465713E}{\isasymsqsubseteq}}\ g\ x{\isaliteral{29}{\isacharparenright}}\ f\ g\ inf{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
 \ fast\isanewline
 \ \ \isacommand{next}\isamarkupfalse%
 \isanewline
 \ \ \ \ \isacommand{fix}\isamarkupfalse%
 \ f\ g\isanewline
 \ \ \ \ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}is{\isacharunderscore}sup\ {\isacharparenleft}{\isasymlambda}f\ g{\isachardot}\ {\isasymforall}x{\isachardot}\ f\ x\ {\isasymsqsubseteq}\ g\ x{\isacharparenright}\ f\ g\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ f\ x\ {\isasymsqunion}\ g\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}partial{\isaliteral{5F}{\isacharunderscore}}order{\isaliteral{2E}{\isachardot}}is{\isaliteral{5F}{\isacharunderscore}}sup\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}f\ g{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ f\ x\ {\isaliteral{5C3C737173756273657465713E}{\isasymsqsubseteq}}\ g\ x{\isaliteral{29}{\isacharparenright}}\ f\ g\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ f\ x\ {\isaliteral{5C3C7371756E696F6E3E}{\isasymsqunion}}\ g\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}rule\ is{\isacharunderscore}supI{\isacharparenright}\ \isacommand{apply}\isamarkupfalse%
-\ rule{\isacharplus}\ \isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}drule\ spec{\isacharcomma}\ assumption{\isacharparenright}{\isacharplus}\ \isacommand{done}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}rule\ is{\isaliteral{5F}{\isacharunderscore}}supI{\isaliteral{29}{\isacharparenright}}\ \isacommand{apply}\isamarkupfalse%
+\ rule{\isaliteral{2B}{\isacharplus}}\ \isacommand{apply}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}drule\ spec{\isaliteral{2C}{\isacharcomma}}\ assumption{\isaliteral{29}{\isacharparenright}}{\isaliteral{2B}{\isacharplus}}\ \isacommand{done}\isamarkupfalse%
 \isanewline
 \ \ \ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymexists}sup{\isachardot}\ partial{\isacharunderscore}order{\isachardot}is{\isacharunderscore}sup\ {\isacharparenleft}{\isasymlambda}f\ g{\isachardot}\ {\isasymforall}x{\isachardot}\ f\ x\ {\isasymsqsubseteq}\ g\ x{\isacharparenright}\ f\ g\ sup{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}sup{\isaliteral{2E}{\isachardot}}\ partial{\isaliteral{5F}{\isacharunderscore}}order{\isaliteral{2E}{\isachardot}}is{\isaliteral{5F}{\isacharunderscore}}sup\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}f\ g{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ f\ x\ {\isaliteral{5C3C737173756273657465713E}{\isasymsqsubseteq}}\ g\ x{\isaliteral{29}{\isacharparenright}}\ f\ g\ sup{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
 \ fast\isanewline
 \ \ \isacommand{qed}\isamarkupfalse%
 %
 \endisatagproof