diff -r 42671298f037 -r 313a24b66a8d doc-src/TutorialI/Misc/document/AdvancedInd.tex
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Sun Nov 07 23:32:26 2010 +0100
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Mon Nov 08 00:00:47 2010 +0100
@@ -40,7 +40,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ hd{\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ last\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 %
 \isadelimproof
 %
@@ -48,7 +48,7 @@
 %
 \isatagproof
 \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}%
+{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ xs{\isaliteral{29}{\isacharparenright}}%
 \begin{isamarkuptxt}%
 \noindent
 But induction produces the warning
@@ -57,14 +57,14 @@
 \end{quote}
 and leads to the base case
 \begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ last\ {\isacharbrackleft}{\isacharbrackright}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ hd\ {\isaliteral{28}{\isacharparenleft}}rev\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ last\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}%
 \end{isabelle}
 Simplification reduces the base case to this:
 \begin{isabelle}
 \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ []
 \end{isabelle}
 We cannot prove this equality because we do not know what \isa{hd} and
-\isa{last} return when applied to \isa{{\isacharbrackleft}{\isacharbrackright}}.
+\isa{last} return when applied to \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}.
 
 We should not have ignored the warning. Because the induction
 formula is only the conclusion, induction does not affect the occurrence of \isa{xs} in the premises.  
@@ -73,12 +73,12 @@
 heuristic applies to rule inductions; see \S\ref{sec:rtc}.}
 \begin{quote}
 \emph{Pull all occurrences of the induction variable into the conclusion
-using \isa{{\isasymlongrightarrow}}.}
+using \isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}}.}
 \end{quote}
 Thus we should state the lemma as an ordinary 
-implication~(\isa{{\isasymlongrightarrow}}), letting
+implication~(\isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}}), letting
 \attrdx{rule_format} (\S\ref{sec:forward}) convert the
-result to the usual \isa{{\isasymLongrightarrow}} form:%
+result to the usual \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} form:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
 %
@@ -89,7 +89,7 @@
 %
 \endisadelimproof
 \isacommand{lemma}\isamarkupfalse%
-\ hd{\isacharunderscore}rev\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequoteclose}%
+\ hd{\isaliteral{5F}{\isacharunderscore}}rev\ {\isaliteral{5B}{\isacharbrackleft}}rule{\isaliteral{5F}{\isacharunderscore}}format{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ hd{\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ last\ xs{\isaliteral{22}{\isachardoublequoteclose}}%
 \isadelimproof
 %
 \endisadelimproof
@@ -100,7 +100,7 @@
 \noindent
 This time, induction leaves us with a trivial base case:
 \begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ last\ {\isacharbrackleft}{\isacharbrackright}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ hd\ {\isaliteral{28}{\isacharparenleft}}rev\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ last\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}%
 \end{isabelle}
 And \isa{auto} completes the proof.
 
@@ -108,9 +108,9 @@
 induction variable, you should turn the conclusion $C$ into
 \[ A@1 \longrightarrow \cdots A@n \longrightarrow C. \]
 Additionally, you may also have to universally quantify some other variables,
-which can yield a fairly complex conclusion.  However, \isa{rule{\isacharunderscore}format} 
-can remove any number of occurrences of \isa{{\isasymforall}} and
-\isa{{\isasymlongrightarrow}}.
+which can yield a fairly complex conclusion.  However, \isa{rule{\isaliteral{5F}{\isacharunderscore}}format} 
+can remove any number of occurrences of \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}} and
+\isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}}.
 
 \index{induction!on a term}%
 A second reason why your proposition may not be amenable to induction is that
@@ -133,7 +133,7 @@
 For an example see \S\ref{sec:CTL-revisited} below.
 
 Of course, all premises that share free variables with $t$ need to be pulled into
-the conclusion as well, under the \isa{{\isasymforall}}, again using \isa{{\isasymlongrightarrow}} as shown above.
+the conclusion as well, under the \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}}, again using \isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}} as shown above.
 
 Readers who are puzzled by the form of statement
 (\ref{eqn:ind-over-term}) above should remember that the
@@ -179,33 +179,33 @@
 induction, where you prove $P(n)$ under the assumption that $P(m)$
 holds for all $m<n$. In Isabelle, this is the theorem \tdx{nat_less_induct}:
 \begin{isabelle}%
-\ \ \ \ \ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n%
+\ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}m{\isaliteral{3C}{\isacharless}}n{\isaliteral{2E}{\isachardot}}\ P\ m\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n%
 \end{isabelle}
 As an application, we prove a property of the following
 function:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{consts}\isamarkupfalse%
-\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
+\ f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \isacommand{axioms}\isamarkupfalse%
-\ f{\isacharunderscore}ax{\isacharcolon}\ {\isachardoublequoteopen}f{\isacharparenleft}f{\isacharparenleft}n{\isacharparenright}{\isacharparenright}\ {\isacharless}\ f{\isacharparenleft}Suc{\isacharparenleft}n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
+\ f{\isaliteral{5F}{\isacharunderscore}}ax{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}f{\isaliteral{28}{\isacharparenleft}}f{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3C}{\isacharless}}\ f{\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
 \begin{isamarkuptext}%
 \begin{warn}
 We discourage the use of axioms because of the danger of
-inconsistencies.  Axiom \isa{f{\isacharunderscore}ax} does
+inconsistencies.  Axiom \isa{f{\isaliteral{5F}{\isacharunderscore}}ax} does
 not introduce an inconsistency because, for example, the identity function
 satisfies it.  Axioms can be useful in exploratory developments, say when 
 you assume some well-known theorems so that you can quickly demonstrate some
 point about methodology.  If your example turns into a substantial proof
 development, you should replace axioms by theorems.
 \end{warn}\noindent
-The axiom for \isa{f} implies \isa{n\ {\isasymle}\ f\ n}, which can
+The axiom for \isa{f} implies \isa{n\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ n}, which can
 be proved by induction on \mbox{\isa{f\ n}}. Following the recipe outlined
 above, we have to phrase the proposition as follows to allow induction:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemma}\isamarkupfalse%
-\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequoteclose}%
+\ f{\isaliteral{5F}{\isacharunderscore}}incr{\isaliteral{5F}{\isacharunderscore}}lem{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{2E}{\isachardot}}\ k\ {\isaliteral{3D}{\isacharequal}}\ f\ i\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ i{\isaliteral{22}{\isachardoublequoteclose}}%
 \isadelimproof
 %
 \endisadelimproof
@@ -214,39 +214,39 @@
 %
 \begin{isamarkuptxt}%
 \noindent
-To perform induction on \isa{k} using \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}, we use
+To perform induction on \isa{k} using \isa{nat{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}induct}, we use
 the same general induction method as for recursion induction (see
 \S\ref{sec:fun-induction}):%
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}induct{\isacharunderscore}tac\ k\ rule{\isacharcolon}\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharparenright}%
+{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ k\ rule{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}induct{\isaliteral{29}{\isacharparenright}}%
 \begin{isamarkuptxt}%
 \noindent
 We get the following proof state:
 \begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ {\isasymforall}i{\isachardot}\ m\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i\ {\isasymLongrightarrow}\ {\isasymforall}i{\isachardot}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}m{\isaliteral{3C}{\isacharless}}n{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{2E}{\isachardot}}\ m\ {\isaliteral{3D}{\isacharequal}}\ f\ i\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ i\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{2E}{\isachardot}}\ n\ {\isaliteral{3D}{\isacharequal}}\ f\ i\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ i%
 \end{isabelle}
-After stripping the \isa{{\isasymforall}i}, the proof continues with a case
-distinction on \isa{i}. The case \isa{i\ {\isacharequal}\ {\isadigit{0}}} is trivial and we focus on
+After stripping the \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i}, the proof continues with a case
+distinction on \isa{i}. The case \isa{i\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}} is trivial and we focus on
 the other case:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}rule\ allI{\isacharparenright}\isanewline
+{\isaliteral{28}{\isacharparenleft}}rule\ allI{\isaliteral{29}{\isacharparenright}}\isanewline
 \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}case{\isacharunderscore}tac\ i{\isacharparenright}\isanewline
+{\isaliteral{28}{\isacharparenleft}}case{\isaliteral{5F}{\isacharunderscore}}tac\ i{\isaliteral{29}{\isacharparenright}}\isanewline
 \ \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}simp{\isacharparenright}%
+{\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{29}{\isacharparenright}}%
 \begin{isamarkuptxt}%
 \begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n\ i\ nat{\isachardot}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}m{\isacharless}n{\isachardot}\ {\isasymforall}i{\isachardot}\ m\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isacharsemicolon}\ i\ {\isacharequal}\ Suc\ nat{\isasymrbrakk}\ {\isasymLongrightarrow}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}n\ i\ nat{\isaliteral{2E}{\isachardot}}\isanewline
+\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}m{\isaliteral{3C}{\isacharless}}n{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{2E}{\isachardot}}\ m\ {\isaliteral{3D}{\isacharequal}}\ f\ i\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ i{\isaliteral{3B}{\isacharsemicolon}}\ i\ {\isaliteral{3D}{\isacharequal}}\ Suc\ nat{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ n\ {\isaliteral{3D}{\isacharequal}}\ f\ i\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ i%
 \end{isabelle}%
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \isacommand{by}\isamarkupfalse%
-{\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ f{\isacharunderscore}ax\ Suc{\isacharunderscore}leI\ intro{\isacharcolon}\ le{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}%
+{\isaliteral{28}{\isacharparenleft}}blast\ intro{\isaliteral{21}{\isacharbang}}{\isaliteral{3A}{\isacharcolon}}\ f{\isaliteral{5F}{\isacharunderscore}}ax\ Suc{\isaliteral{5F}{\isacharunderscore}}leI\ intro{\isaliteral{3A}{\isacharcolon}}\ le{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}trans{\isaliteral{29}{\isacharparenright}}%
 \endisatagproof
 {\isafoldproof}%
 %
@@ -258,42 +258,42 @@
 \noindent
 If you find the last step puzzling, here are the two lemmas it employs:
 \begin{isabelle}
-\isa{m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ Suc\ m\ {\isasymle}\ n}
+\isa{m\ {\isaliteral{3C}{\isacharless}}\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Suc\ m\ {\isaliteral{5C3C6C653E}{\isasymle}}\ n}
 \rulename{Suc_leI}\isanewline
-\isa{{\isasymlbrakk}x\ {\isasymle}\ y{\isacharsemicolon}\ y\ {\isacharless}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}\ z}
+\isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}x\ {\isaliteral{5C3C6C653E}{\isasymle}}\ y{\isaliteral{3B}{\isacharsemicolon}}\ y\ {\isaliteral{3C}{\isacharless}}\ z{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{3C}{\isacharless}}\ z}
 \rulename{le_less_trans}
 \end{isabelle}
 %
 The proof goes like this (writing \isa{j} instead of \isa{nat}).
-Since \isa{i\ {\isacharequal}\ Suc\ j} it suffices to show
-\hbox{\isa{j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}}},
-by \isa{Suc{\isacharunderscore}leI}\@.  This is
-proved as follows. From \isa{f{\isacharunderscore}ax} we have \isa{f\ {\isacharparenleft}f\ j{\isacharparenright}\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}}
-(1) which implies \isa{f\ j\ {\isasymle}\ f\ {\isacharparenleft}f\ j{\isacharparenright}} by the induction hypothesis.
-Using (1) once more we obtain \isa{f\ j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (2) by the transitivity
-rule \isa{le{\isacharunderscore}less{\isacharunderscore}trans}.
-Using the induction hypothesis once more we obtain \isa{j\ {\isasymle}\ f\ j}
-which, together with (2) yields \isa{j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (again by
-\isa{le{\isacharunderscore}less{\isacharunderscore}trans}).
+Since \isa{i\ {\isaliteral{3D}{\isacharequal}}\ Suc\ j} it suffices to show
+\hbox{\isa{j\ {\isaliteral{3C}{\isacharless}}\ f\ {\isaliteral{28}{\isacharparenleft}}Suc\ j{\isaliteral{29}{\isacharparenright}}}},
+by \isa{Suc{\isaliteral{5F}{\isacharunderscore}}leI}\@.  This is
+proved as follows. From \isa{f{\isaliteral{5F}{\isacharunderscore}}ax} we have \isa{f\ {\isaliteral{28}{\isacharparenleft}}f\ j{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3C}{\isacharless}}\ f\ {\isaliteral{28}{\isacharparenleft}}Suc\ j{\isaliteral{29}{\isacharparenright}}}
+(1) which implies \isa{f\ j\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ {\isaliteral{28}{\isacharparenleft}}f\ j{\isaliteral{29}{\isacharparenright}}} by the induction hypothesis.
+Using (1) once more we obtain \isa{f\ j\ {\isaliteral{3C}{\isacharless}}\ f\ {\isaliteral{28}{\isacharparenleft}}Suc\ j{\isaliteral{29}{\isacharparenright}}} (2) by the transitivity
+rule \isa{le{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}trans}.
+Using the induction hypothesis once more we obtain \isa{j\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ j}
+which, together with (2) yields \isa{j\ {\isaliteral{3C}{\isacharless}}\ f\ {\isaliteral{28}{\isacharparenleft}}Suc\ j{\isaliteral{29}{\isacharparenright}}} (again by
+\isa{le{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}trans}).
 
 This last step shows both the power and the danger of automatic proofs.  They
 will usually not tell you how the proof goes, because it can be hard to
 translate the internal proof into a human-readable format.  Automatic
 proofs are easy to write but hard to read and understand.
 
-The desired result, \isa{i\ {\isasymle}\ f\ i}, follows from \isa{f{\isacharunderscore}incr{\isacharunderscore}lem}:%
+The desired result, \isa{i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ i}, follows from \isa{f{\isaliteral{5F}{\isacharunderscore}}incr{\isaliteral{5F}{\isacharunderscore}}lem}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemmas}\isamarkupfalse%
-\ f{\isacharunderscore}incr\ {\isacharequal}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}%
+\ f{\isaliteral{5F}{\isacharunderscore}}incr\ {\isaliteral{3D}{\isacharequal}}\ f{\isaliteral{5F}{\isacharunderscore}}incr{\isaliteral{5F}{\isacharunderscore}}lem{\isaliteral{5B}{\isacharbrackleft}}rule{\isaliteral{5F}{\isacharunderscore}}format{\isaliteral{2C}{\isacharcomma}}\ OF\ refl{\isaliteral{5D}{\isacharbrackright}}%
 \begin{isamarkuptext}%
 \noindent
-The final \isa{refl} gets rid of the premise \isa{{\isacharquery}k\ {\isacharequal}\ f\ {\isacharquery}i}. 
+The final \isa{refl} gets rid of the premise \isa{{\isaliteral{3F}{\isacharquery}}k\ {\isaliteral{3D}{\isacharequal}}\ f\ {\isaliteral{3F}{\isacharquery}}i}. 
 We could have included this derivation in the original statement of the lemma:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemma}\isamarkupfalse%
-\ f{\isacharunderscore}incr{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequoteclose}%
+\ f{\isaliteral{5F}{\isacharunderscore}}incr{\isaliteral{5B}{\isacharbrackleft}}rule{\isaliteral{5F}{\isacharunderscore}}format{\isaliteral{2C}{\isacharcomma}}\ OF\ refl{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{2E}{\isachardot}}\ k\ {\isaliteral{3D}{\isacharequal}}\ f\ i\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ i{\isaliteral{22}{\isachardoublequoteclose}}%
 \isadelimproof
 %
 \endisadelimproof
@@ -317,18 +317,18 @@
 whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the
 format is
 \begin{quote}
-\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $y@1 \dots y@n$ \isa{rule{\isacharcolon}} $r$\isa{{\isacharparenright}}
+\isacommand{apply}\isa{{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac} $y@1 \dots y@n$ \isa{rule{\isaliteral{3A}{\isacharcolon}}} $r$\isa{{\isaliteral{29}{\isacharparenright}}}
 \end{quote}
 where $y@1, \dots, y@n$ are variables in the conclusion of the first subgoal.
 
-A further useful induction rule is \isa{length{\isacharunderscore}induct},
+A further useful induction rule is \isa{length{\isaliteral{5F}{\isacharunderscore}}induct},
 induction on the length of a list\indexbold{*length_induct}
 \begin{isabelle}%
-\ \ \ \ \ {\isacharparenleft}{\isasymAnd}xs{\isachardot}\ {\isasymforall}ys{\isachardot}\ length\ ys\ {\isacharless}\ length\ xs\ {\isasymlongrightarrow}\ P\ ys\ {\isasymLongrightarrow}\ P\ xs{\isacharparenright}\ {\isasymLongrightarrow}\ P\ xs%
+\ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}xs{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}ys{\isaliteral{2E}{\isachardot}}\ length\ ys\ {\isaliteral{3C}{\isacharless}}\ length\ xs\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ P\ ys\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ xs%
 \end{isabelle}
-which is a special case of \isa{measure{\isacharunderscore}induct}
+which is a special case of \isa{measure{\isaliteral{5F}{\isacharunderscore}}induct}
 \begin{isabelle}%
-\ \ \ \ \ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ {\isasymforall}y{\isachardot}\ f\ y\ {\isacharless}\ f\ x\ {\isasymlongrightarrow}\ P\ y\ {\isasymLongrightarrow}\ P\ x{\isacharparenright}\ {\isasymLongrightarrow}\ P\ a%
+\ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}y{\isaliteral{2E}{\isachardot}}\ f\ y\ {\isaliteral{3C}{\isacharless}}\ f\ x\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ P\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ a%
 \end{isabelle}
 where \isa{f} may be any function into type \isa{nat}.%
 \end{isamarkuptext}%
@@ -343,13 +343,13 @@
 \index{induction!deriving new schemas}%
 Induction schemas are ordinary theorems and you can derive new ones
 whenever you wish.  This section shows you how, using the example
-of \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}. Assume we only have structural induction
+of \isa{nat{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}induct}. Assume we only have structural induction
 available for \isa{nat} and want to derive complete induction.  We
 must generalize the statement as shown:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemma}\isamarkupfalse%
-\ induct{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymAnd}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m{\isachardoublequoteclose}\isanewline
+\ induct{\isaliteral{5F}{\isacharunderscore}}lem{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}m{\isaliteral{3C}{\isacharless}}n{\isaliteral{2E}{\isachardot}}\ P\ m\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}m{\isaliteral{3C}{\isacharless}}n{\isaliteral{2E}{\isachardot}}\ P\ m{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 %
 \isadelimproof
 %
@@ -357,18 +357,18 @@
 %
 \isatagproof
 \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}%
+{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ n{\isaliteral{29}{\isacharparenright}}%
 \begin{isamarkuptxt}%
 \noindent
-The base case is vacuously true. For the induction step (\isa{m\ {\isacharless}\ Suc\ n}) we distinguish two cases: case \isa{m\ {\isacharless}\ n} is true by induction
-hypothesis and case \isa{m\ {\isacharequal}\ n} follows from the assumption, again using
+The base case is vacuously true. For the induction step (\isa{m\ {\isaliteral{3C}{\isacharless}}\ Suc\ n}) we distinguish two cases: case \isa{m\ {\isaliteral{3C}{\isacharless}}\ n} is true by induction
+hypothesis and case \isa{m\ {\isaliteral{3D}{\isacharequal}}\ n} follows from the assumption, again using
 the induction hypothesis:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \ \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}blast{\isacharparenright}\isanewline
+{\isaliteral{28}{\isacharparenleft}}blast{\isaliteral{29}{\isacharparenright}}\isanewline
 \isacommand{by}\isamarkupfalse%
-{\isacharparenleft}blast\ elim{\isacharcolon}\ less{\isacharunderscore}SucE{\isacharparenright}%
+{\isaliteral{28}{\isacharparenleft}}blast\ elim{\isaliteral{3A}{\isacharcolon}}\ less{\isaliteral{5F}{\isacharunderscore}}SucE{\isaliteral{29}{\isacharparenright}}%
 \endisatagproof
 {\isafoldproof}%
 %
@@ -378,21 +378,21 @@
 %
 \begin{isamarkuptext}%
 \noindent
-The elimination rule \isa{less{\isacharunderscore}SucE} expresses the case distinction:
+The elimination rule \isa{less{\isaliteral{5F}{\isacharunderscore}}SucE} expresses the case distinction:
 \begin{isabelle}%
-\ \ \ \ \ {\isasymlbrakk}m\ {\isacharless}\ Suc\ n{\isacharsemicolon}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ m\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
+\ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}m\ {\isaliteral{3C}{\isacharless}}\ Suc\ n{\isaliteral{3B}{\isacharsemicolon}}\ m\ {\isaliteral{3C}{\isacharless}}\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{3B}{\isacharsemicolon}}\ m\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P%
 \end{isabelle}
 
 Now it is straightforward to derive the original version of
-\isa{nat{\isacharunderscore}less{\isacharunderscore}induct} by manipulating the conclusion of the above
+\isa{nat{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}induct} by manipulating the conclusion of the above
 lemma: instantiate \isa{n} by \isa{Suc\ n} and \isa{m} by \isa{n}
-and remove the trivial condition \isa{n\ {\isacharless}\ Suc\ n}. Fortunately, this
+and remove the trivial condition \isa{n\ {\isaliteral{3C}{\isacharless}}\ Suc\ n}. Fortunately, this
 happens automatically when we add the lemma as a new premise to the
 desired goal:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{theorem}\isamarkupfalse%
-\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymAnd}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n{\isachardoublequoteclose}\isanewline
+\ nat{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}induct{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}m{\isaliteral{3C}{\isacharless}}n{\isaliteral{2E}{\isachardot}}\ P\ m\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 %
 \isadelimproof
 %
@@ -400,7 +400,7 @@
 %
 \isatagproof
 \isacommand{by}\isamarkupfalse%
-{\isacharparenleft}insert\ induct{\isacharunderscore}lem{\isacharcomma}\ blast{\isacharparenright}%
+{\isaliteral{28}{\isacharparenleft}}insert\ induct{\isaliteral{5F}{\isacharunderscore}}lem{\isaliteral{2C}{\isacharcomma}}\ blast{\isaliteral{29}{\isacharparenright}}%
 \endisatagproof
 {\isafoldproof}%
 %
@@ -411,8 +411,8 @@
 \begin{isamarkuptext}%
 HOL already provides the mother of
 all inductions, well-founded induction (see \S\ref{sec:Well-founded}).  For
-example theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} is
-a special case of \isa{wf{\isacharunderscore}induct} where \isa{r} is \isa{{\isacharless}} on
+example theorem \isa{nat{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}induct} is
+a special case of \isa{wf{\isaliteral{5F}{\isacharunderscore}}induct} where \isa{r} is \isa{{\isaliteral{3C}{\isacharless}}} on
 \isa{nat}. The details can be found in theory \isa{Wellfounded_Recursion}.%
 \end{isamarkuptext}%
 \isamarkuptrue%