doc-src/TutorialI/Misc/document/asm_simp.tex

 %
 \begin{isamarkuptext}%
 By default, assumptions are part of the simplification process: they are used
 as simplification rules and are simplified themselves. For example:%
 \end{isamarkuptext}%
-\isacommand{lemma}\ {"}{\isasymlbrakk}\ xs\ @\ zs\ =\ ys\ @\ xs;\ []\ @\ xs\ =\ []\ @\ []\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ ys\ =\ zs{"}\isanewline
+\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ xs\ {\isacharat}\ zs\ {\isacharequal}\ ys\ {\isacharat}\ xs{\isacharsemicolon}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ ys\ {\isacharequal}\ zs{\isachardoublequote}\isanewline
 \isacommand{by}\ simp%
 \begin{isamarkuptext}%
 \noindent
-The second assumption simplifies to \isa{\mbox{xs}\ =\ []}, which in turn
-simplifies the first assumption to \isa{\mbox{zs}\ =\ \mbox{ys}}, thus reducing the
-conclusion to \isa{\mbox{ys}\ =\ \mbox{ys}} and hence to \isa{True}.
+The second assumption simplifies to \isa{\mbox{xs}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}, which in turn
+simplifies the first assumption to \isa{\mbox{zs}\ {\isacharequal}\ \mbox{ys}}, thus reducing the
+conclusion to \isa{\mbox{ys}\ {\isacharequal}\ \mbox{ys}} and hence to \isa{True}.
 
 In some cases this may be too much of a good thing and may lead to
 nontermination:%
 \end{isamarkuptext}%
-\isacommand{lemma}\ {"}{\isasymforall}x.\ f\ x\ =\ g\ (f\ (g\ x))\ {\isasymLongrightarrow}\ f\ []\ =\ f\ []\ @\ []{"}%
+\isacommand{lemma}\ {\isachardoublequote}{\isasymforall}x{\isachardot}\ f\ x\ {\isacharequal}\ g\ {\isacharparenleft}f\ {\isacharparenleft}g\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}%
 \begin{isamarkuptxt}%
 \noindent
 cannot be solved by an unmodified application of \isa{simp} because the
-simplification rule \isa{\mbox{f}\ \mbox{x}\ =\ \mbox{g}\ (\mbox{f}\ (\mbox{g}\ \mbox{x}))} extracted from the assumption
+simplification rule \isa{\mbox{f}\ \mbox{x}\ {\isacharequal}\ \mbox{g}\ {\isacharparenleft}\mbox{f}\ {\isacharparenleft}\mbox{g}\ \mbox{x}{\isacharparenright}{\isacharparenright}} extracted from the assumption
 does not terminate. Isabelle notices certain simple forms of
 nontermination but not this one. The problem can be circumvented by
 explicitly telling the simplifier to ignore the assumptions:%
 \end{isamarkuptxt}%
-\isacommand{by}(simp\ (no\_asm))%
+\isacommand{by}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
 There are three options that influence the treatment of assumptions:
 \begin{description}
 \item[\isa{(no_asm)}]\indexbold{*no_asm}