doc-src/TutorialI/Types/document/Overloading.tex

 \isamarkupsubsubsection{Overloading%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-We can introduce a binary infix addition operator \isa{{\isasymotimes}}
+We can introduce a binary infix addition operator \isa{{\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}}
 for arbitrary types by means of a type class:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{class}\isamarkupfalse%
-\ plus\ {\isacharequal}\isanewline
-\ \ \isakeyword{fixes}\ plus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}%
+\ plus\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ \isakeyword{fixes}\ plus\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F706C75733E}{\isasymoplus}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{7}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}%
 \begin{isamarkuptext}%
 \noindent This introduces a new class \isa{plus},
 along with a constant \isa{plus} with nice infix syntax.
 \isa{plus} is also named \emph{class operation}.  The type
-of \isa{plus} carries a class constraint \isa{{\isachardoublequote}{\isacharprime}a\ {\isacharcolon}{\isacharcolon}\ plus{\isachardoublequote}} on its type variable, meaning that only types of class
-\isa{plus} can be instantiated for \isa{{\isachardoublequote}{\isacharprime}a{\isachardoublequote}}.
+of \isa{plus} carries a class constraint \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ plus{\isaliteral{22}{\isachardoublequote}}} on its type variable, meaning that only types of class
+\isa{plus} can be instantiated for \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}}.
 To breathe life into \isa{plus} we need to declare a type
 to be an \bfindex{instance} of \isa{plus}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{instantiation}\isamarkupfalse%
-\ nat\ {\isacharcolon}{\isacharcolon}\ plus\isanewline
+\ nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ plus\isanewline
 \isakeyword{begin}%
 \begin{isamarkuptext}%
 \noindent Command \isacommand{instantiation} opens a local
 theory context.  Here we can now instantiate \isa{plus} on
 \isa{nat}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{primrec}\isamarkupfalse%
-\ plus{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isasymoplus}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
-\ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymoplus}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}m\ {\isasymoplus}\ n{\isacharparenright}{\isachardoublequoteclose}%
+\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
+\ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ n\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}Suc\ m\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ n\ {\isaliteral{3D}{\isacharequal}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
 \begin{isamarkuptext}%
 \noindent Note that the name \isa{plus} carries a
-suffix \isa{{\isacharunderscore}nat}; by default, the local name of a class operation
-\isa{f} to be instantiated on type constructor \isa{{\isasymkappa}} is mangled
-as \isa{f{\isacharunderscore}{\isasymkappa}}.  In case of uncertainty, these names may be inspected
-using the \hyperlink{command.print-context}{\mbox{\isa{\isacommand{print{\isacharunderscore}context}}}} command or the corresponding
+suffix \isa{{\isaliteral{5F}{\isacharunderscore}}nat}; by default, the local name of a class operation
+\isa{f} to be instantiated on type constructor \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} is mangled
+as \isa{f{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}}.  In case of uncertainty, these names may be inspected
+using the \hyperlink{command.print-context}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}context}}}} command or the corresponding
 ProofGeneral button.
 
 Although class \isa{plus} has no axioms, the instantiation must be
 formally concluded by a (trivial) instantiation proof ``..'':%
 \end{isamarkuptext}%

 \isadelimproof
 \ %
 \endisadelimproof
 %
 \isatagproof
-\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
 %
 \isadelimproof

 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{end}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
-\noindent From now on, terms like \isa{Suc\ {\isacharparenleft}m\ {\isasymoplus}\ {\isadigit{2}}{\isacharparenright}} are
+\noindent From now on, terms like \isa{Suc\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} are
 legal.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{instantiation}\isamarkupfalse%
-\ prod\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}plus{\isacharcomma}\ plus{\isacharparenright}\ plus\isanewline
+\ prod\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}plus{\isaliteral{2C}{\isacharcomma}}\ plus{\isaliteral{29}{\isacharparenright}}\ plus\isanewline
 \isakeyword{begin}%
 \begin{isamarkuptext}%
 \noindent Here we instantiate the product type \isa{prod} to
 class \isa{plus}, given that its type arguments are of
 class \isa{plus}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{fun}\isamarkupfalse%
-\ plus{\isacharunderscore}prod\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymoplus}\ {\isacharparenleft}w{\isacharcomma}\ z{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymoplus}\ w{\isacharcomma}\ y\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequoteclose}%
+\ plus{\isaliteral{5F}{\isacharunderscore}}prod\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
+\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ {\isaliteral{28}{\isacharparenleft}}w{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ w{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ z{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
 \begin{isamarkuptext}%
 \noindent Obviously, overloaded specifications may include
 recursion over the syntactic structure of types.%
 \end{isamarkuptext}%
 \isamarkuptrue%

 \isadelimproof
 \ %
 \endisadelimproof
 %
 \isatagproof
-\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
 %
 \isadelimproof