doc-src/IsarRef/Thy/document/ML_Tactic.tex

 %
 \begin{isabellebody}%
-\def\isabellecontext{ML{\isacharunderscore}Tactic}%
+\def\isabellecontext{ML{\isaliteral{5F}{\isacharunderscore}}Tactic}%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
-\ ML{\isacharunderscore}Tactic\isanewline
+\ ML{\isaliteral{5F}{\isacharunderscore}}Tactic\isanewline
 \isakeyword{imports}\ Main\isanewline
 \isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%
 %

   \item Abbreviations for singleton arguments (e.g.\ \verb|resolve_tac|
   vs.\ \verb|rtac|).
 
   \end{enumerate}
 
-  Basically, the set of Isar tactic emulations \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}},
-  \hyperlink{method.erule-tac}{\mbox{\isa{erule{\isacharunderscore}tac}}}, \hyperlink{method.drule-tac}{\mbox{\isa{drule{\isacharunderscore}tac}}}, \hyperlink{method.frule-tac}{\mbox{\isa{frule{\isacharunderscore}tac}}} (see
+  Basically, the set of Isar tactic emulations \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}tac}}},
+  \hyperlink{method.erule-tac}{\mbox{\isa{erule{\isaliteral{5F}{\isacharunderscore}}tac}}}, \hyperlink{method.drule-tac}{\mbox{\isa{drule{\isaliteral{5F}{\isacharunderscore}}tac}}}, \hyperlink{method.frule-tac}{\mbox{\isa{frule{\isaliteral{5F}{\isacharunderscore}}tac}}} (see
   \secref{sec:tactics}) would be sufficient to cover the four modes,
   either with or without instantiation, and either with single or
   multiple arguments.  Although it is more convenient in most cases to
   use the plain \hyperlink{method.rule}{\mbox{\isa{rule}}} method (see
   \secref{sec:pure-meth-att}), or any of its ``improper'' variants
   \hyperlink{method.erule}{\mbox{\isa{erule}}}, \hyperlink{method.drule}{\mbox{\isa{drule}}}, \hyperlink{method.frule}{\mbox{\isa{frule}}} (see
   \secref{sec:misc-meth-att}).  Note that explicit goal addressing is
-  only supported by the actual \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}} version.
+  only supported by the actual \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}tac}}} version.
 
   With this in mind, plain resolution tactics correspond to Isar
   methods as follows.
 
   \medskip
   \begin{tabular}{lll}
-    \verb|rtac|~\isa{{\isachardoublequote}a\ {\isadigit{1}}{\isachardoublequote}} & & \isa{{\isachardoublequote}rule\ a{\isachardoublequote}} \\
-    \verb|resolve_tac|~\isa{{\isachardoublequote}{\isacharbrackleft}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}\ {\isadigit{1}}{\isachardoublequote}} & & \isa{{\isachardoublequote}rule\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}{\isachardoublequote}} \\
-    \verb|res_inst_tac|~\isa{{\isachardoublequote}ctxt\ {\isacharbrackleft}{\isacharparenleft}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ t\isactrlsub {\isadigit{1}}{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}\ a\ {\isadigit{1}}{\isachardoublequote}} & &
-    \isa{{\isachardoublequote}rule{\isacharunderscore}tac\ x\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ {\isasymIN}\ a{\isachardoublequote}} \\[0.5ex]
-    \verb|rtac|~\isa{{\isachardoublequote}a\ i{\isachardoublequote}} & & \isa{{\isachardoublequote}rule{\isacharunderscore}tac\ {\isacharbrackleft}i{\isacharbrackright}\ a{\isachardoublequote}} \\
-    \verb|resolve_tac|~\isa{{\isachardoublequote}{\isacharbrackleft}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}\ i{\isachardoublequote}} & & \isa{{\isachardoublequote}rule{\isacharunderscore}tac\ {\isacharbrackleft}i{\isacharbrackright}\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}{\isachardoublequote}} \\
-    \verb|res_inst_tac|~\isa{{\isachardoublequote}ctxt\ {\isacharbrackleft}{\isacharparenleft}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ t\isactrlsub {\isadigit{1}}{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}\ a\ i{\isachardoublequote}} & &
-    \isa{{\isachardoublequote}rule{\isacharunderscore}tac\ {\isacharbrackleft}i{\isacharbrackright}\ x\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ {\isasymIN}\ a{\isachardoublequote}} \\
+    \verb|rtac|~\isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} & & \isa{{\isaliteral{22}{\isachardoublequote}}rule\ a{\isaliteral{22}{\isachardoublequote}}} \\
+    \verb|resolve_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5D}{\isacharbrackright}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} & & \isa{{\isaliteral{22}{\isachardoublequote}}rule\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \\
+    \verb|res_inst_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}ctxt\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5D}{\isacharbrackright}}\ a\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} & &
+    \isa{{\isaliteral{22}{\isachardoublequote}}rule{\isaliteral{5F}{\isacharunderscore}}tac\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C494E3E}{\isasymIN}}\ a{\isaliteral{22}{\isachardoublequote}}} \\[0.5ex]
+    \verb|rtac|~\isa{{\isaliteral{22}{\isachardoublequote}}a\ i{\isaliteral{22}{\isachardoublequote}}} & & \isa{{\isaliteral{22}{\isachardoublequote}}rule{\isaliteral{5F}{\isacharunderscore}}tac\ {\isaliteral{5B}{\isacharbrackleft}}i{\isaliteral{5D}{\isacharbrackright}}\ a{\isaliteral{22}{\isachardoublequote}}} \\
+    \verb|resolve_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5D}{\isacharbrackright}}\ i{\isaliteral{22}{\isachardoublequote}}} & & \isa{{\isaliteral{22}{\isachardoublequote}}rule{\isaliteral{5F}{\isacharunderscore}}tac\ {\isaliteral{5B}{\isacharbrackleft}}i{\isaliteral{5D}{\isacharbrackright}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \\
+    \verb|res_inst_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}ctxt\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5D}{\isacharbrackright}}\ a\ i{\isaliteral{22}{\isachardoublequote}}} & &
+    \isa{{\isaliteral{22}{\isachardoublequote}}rule{\isaliteral{5F}{\isacharunderscore}}tac\ {\isaliteral{5B}{\isacharbrackleft}}i{\isaliteral{5D}{\isacharbrackright}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C494E3E}{\isasymIN}}\ a{\isaliteral{22}{\isachardoublequote}}} \\
   \end{tabular}
   \medskip
 
   Note that explicit goal addressing may be usually avoided by
   changing the order of subgoals with \hyperlink{command.defer}{\mbox{\isa{\isacommand{defer}}}} or \hyperlink{command.prefer}{\mbox{\isa{\isacommand{prefer}}}} (see \secref{sec:tactic-commands}).%

 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
 The main Simplifier tactics \verb|simp_tac| and variants (cf.\
   \cite{isabelle-ref}) are all covered by the \hyperlink{method.simp}{\mbox{\isa{simp}}} and
-  \hyperlink{method.simp-all}{\mbox{\isa{simp{\isacharunderscore}all}}} methods (see \secref{sec:simplifier}).  Note that
+  \hyperlink{method.simp-all}{\mbox{\isa{simp{\isaliteral{5F}{\isacharunderscore}}all}}} methods (see \secref{sec:simplifier}).  Note that
   there is no individual goal addressing available, simplification
   acts either on the first goal (\hyperlink{method.simp}{\mbox{\isa{simp}}}) or all goals
-  (\hyperlink{method.simp-all}{\mbox{\isa{simp{\isacharunderscore}all}}}).
-
-  \medskip
-  \begin{tabular}{lll}
-    \verb|asm_full_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}} \\
-    \verb|ALLGOALS|~(\verb|asm_full_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}{\isachardoublequote}}) & & \hyperlink{method.simp-all}{\mbox{\isa{simp{\isacharunderscore}all}}} \\[0.5ex]
-    \verb|simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}}~\isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isachardoublequote}} \\
-    \verb|asm_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}}~\isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}{\isachardoublequote}} \\
-    \verb|full_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}}~\isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}{\isachardoublequote}} \\
-    \verb|asm_lr_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}}~\isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharunderscore}lr{\isacharparenright}{\isachardoublequote}} \\
+  (\hyperlink{method.simp-all}{\mbox{\isa{simp{\isaliteral{5F}{\isacharunderscore}}all}}}).
+
+  \medskip
+  \begin{tabular}{lll}
+    \verb|asm_full_simp_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}simpset{\isaliteral{7D}{\isacharbraceright}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}} \\
+    \verb|ALLGOALS|~(\verb|asm_full_simp_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}simpset{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}}) & & \hyperlink{method.simp-all}{\mbox{\isa{simp{\isaliteral{5F}{\isacharunderscore}}all}}} \\[0.5ex]
+    \verb|simp_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}simpset{\isaliteral{7D}{\isacharbraceright}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
+    \verb|asm_simp_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}simpset{\isaliteral{7D}{\isacharbraceright}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
+    \verb|full_simp_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}simpset{\isaliteral{7D}{\isacharbraceright}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{5F}{\isacharunderscore}}use{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
+    \verb|asm_lr_simp_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}simpset{\isaliteral{7D}{\isacharbraceright}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}asm{\isaliteral{5F}{\isacharunderscore}}lr{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   \end{tabular}
   \medskip%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %

   Isabelle/HOL, some of these also in Isabelle/FOL or Isabelle/ZF.
   The most common ones of these may be ported to Isar as follows.
 
   \medskip
   \begin{tabular}{lll}
-    \verb|stac|~\isa{{\isachardoublequote}a\ {\isadigit{1}}{\isachardoublequote}} & & \isa{{\isachardoublequote}subst\ a{\isachardoublequote}} \\
+    \verb|stac|~\isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} & & \isa{{\isaliteral{22}{\isachardoublequote}}subst\ a{\isaliteral{22}{\isachardoublequote}}} \\
     \verb|hyp_subst_tac|~\isa{{\isadigit{1}}} & & \isa{hypsubst} \\
-    \verb|strip_tac|~\isa{{\isadigit{1}}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} & \isa{{\isachardoublequote}intro\ strip{\isachardoublequote}} \\
-    \verb|split_all_tac|~\isa{{\isadigit{1}}} & & \isa{{\isachardoublequote}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}\ only{\isacharcolon}\ split{\isacharunderscore}tupled{\isacharunderscore}all{\isachardoublequote}} \\
-      & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} & \isa{{\isachardoublequote}simp\ only{\isacharcolon}\ split{\isacharunderscore}tupled{\isacharunderscore}all{\isachardoublequote}} \\
-      & \isa{{\isachardoublequote}{\isasymlless}{\isachardoublequote}} & \isa{{\isachardoublequote}clarify{\isachardoublequote}} \\
+    \verb|strip_tac|~\isa{{\isadigit{1}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C617070726F783E}{\isasymapprox}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}intro\ strip{\isaliteral{22}{\isachardoublequote}}} \\
+    \verb|split_all_tac|~\isa{{\isadigit{1}}} & & \isa{{\isaliteral{22}{\isachardoublequote}}simp\ {\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{29}{\isacharparenright}}\ only{\isaliteral{3A}{\isacharcolon}}\ split{\isaliteral{5F}{\isacharunderscore}}tupled{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{22}{\isachardoublequote}}} \\
+      & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C617070726F783E}{\isasymapprox}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}simp\ only{\isaliteral{3A}{\isacharcolon}}\ split{\isaliteral{5F}{\isacharunderscore}}tupled{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{22}{\isachardoublequote}}} \\
+      & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C6C6573733E}{\isasymlless}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}clarify{\isaliteral{22}{\isachardoublequote}}} \\
   \end{tabular}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isamarkupsection{Tacticals%

 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
 Classic Isabelle provides a huge amount of tacticals for combination
   and modification of existing tactics.  This has been greatly reduced
-  in Isar, providing the bare minimum of combinators only: ``\isa{{\isachardoublequote}{\isacharcomma}{\isachardoublequote}}'' (sequential composition), ``\isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}'' (alternative
-  choices), ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' (try), ``\isa{{\isachardoublequote}{\isacharplus}{\isachardoublequote}}'' (repeat at least
+  in Isar, providing the bare minimum of combinators only: ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}}'' (sequential composition), ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}}'' (alternative
+  choices), ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' (try), ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{22}{\isachardoublequote}}}'' (repeat at least
   once).  These are usually sufficient in practice; if all fails,
   arbitrary ML tactic code may be invoked via the \hyperlink{method.tactic}{\mbox{\isa{tactic}}}
   method (see \secref{sec:tactics}).
 
   \medskip Common ML tacticals may be expressed directly in Isar as
   follows:
 
   \medskip
   \begin{tabular}{lll}
-    \isa{{\isachardoublequote}tac\isactrlsub {\isadigit{1}}{\isachardoublequote}}~\verb|THEN|~\isa{{\isachardoublequote}tac\isactrlsub {\isadigit{2}}{\isachardoublequote}} & & \isa{{\isachardoublequote}meth\isactrlsub {\isadigit{1}}{\isacharcomma}\ meth\isactrlsub {\isadigit{2}}{\isachardoublequote}} \\
-    \isa{{\isachardoublequote}tac\isactrlsub {\isadigit{1}}{\isachardoublequote}}~\verb|ORELSE|~\isa{{\isachardoublequote}tac\isactrlsub {\isadigit{2}}{\isachardoublequote}} & & \isa{{\isachardoublequote}meth\isactrlsub {\isadigit{1}}\ {\isacharbar}\ meth\isactrlsub {\isadigit{2}}{\isachardoublequote}} \\
-    \verb|TRY|~\isa{tac} & & \isa{{\isachardoublequote}meth{\isacharquery}{\isachardoublequote}} \\
-    \verb|REPEAT1|~\isa{tac} & & \isa{{\isachardoublequote}meth{\isacharplus}{\isachardoublequote}} \\
-    \verb|REPEAT|~\isa{tac} & & \isa{{\isachardoublequote}{\isacharparenleft}meth{\isacharplus}{\isacharparenright}{\isacharquery}{\isachardoublequote}} \\
-    \verb|EVERY|~\isa{{\isachardoublequote}{\isacharbrackleft}tac\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}{\isachardoublequote}} & & \isa{{\isachardoublequote}meth\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isachardoublequote}} \\
-    \verb|FIRST|~\isa{{\isachardoublequote}{\isacharbrackleft}tac\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}{\isachardoublequote}} & & \isa{{\isachardoublequote}meth\isactrlsub {\isadigit{1}}\ {\isacharbar}\ {\isasymdots}{\isachardoublequote}} \\
+    \isa{{\isaliteral{22}{\isachardoublequote}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}~\verb|THEN|~\isa{{\isaliteral{22}{\isachardoublequote}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} & & \isa{{\isaliteral{22}{\isachardoublequote}}meth\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ meth\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} \\
+    \isa{{\isaliteral{22}{\isachardoublequote}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}~\verb|ORELSE|~\isa{{\isaliteral{22}{\isachardoublequote}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} & & \isa{{\isaliteral{22}{\isachardoublequote}}meth\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{7C}{\isacharbar}}\ meth\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} \\
+    \verb|TRY|~\isa{tac} & & \isa{{\isaliteral{22}{\isachardoublequote}}meth{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}} \\
+    \verb|REPEAT1|~\isa{tac} & & \isa{{\isaliteral{22}{\isachardoublequote}}meth{\isaliteral{2B}{\isacharplus}}{\isaliteral{22}{\isachardoublequote}}} \\
+    \verb|REPEAT|~\isa{tac} & & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}meth{\isaliteral{2B}{\isacharplus}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}} \\
+    \verb|EVERY|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} & & \isa{{\isaliteral{22}{\isachardoublequote}}meth\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \\
+    \verb|FIRST|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} & & \isa{{\isaliteral{22}{\isachardoublequote}}meth\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \\
   \end{tabular}
   \medskip
 
   \medskip \verb|CHANGED| (see \cite{isabelle-ref}) is usually not
   required in Isar, since most basic proof methods already fail unless
-  there is an actual change in the goal state.  Nevertheless, ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}''  (try) may be used to accept \emph{unchanged} results as
+  there is an actual change in the goal state.  Nevertheless, ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}''  (try) may be used to accept \emph{unchanged} results as
   well.
 
   \medskip \verb|ALLGOALS|, \verb|SOMEGOAL| etc.\ (see
   \cite{isabelle-ref}) are not available in Isar, since there is no
   direct goal addressing.  Nevertheless, some basic methods address
-  all goals internally, notably \hyperlink{method.simp-all}{\mbox{\isa{simp{\isacharunderscore}all}}} (see
+  all goals internally, notably \hyperlink{method.simp-all}{\mbox{\isa{simp{\isaliteral{5F}{\isacharunderscore}}all}}} (see
   \secref{sec:simplifier}).  Also note that \verb|ALLGOALS| can be
-  often replaced by ``\isa{{\isachardoublequote}{\isacharplus}{\isachardoublequote}}'' (repeat at least once), although
+  often replaced by ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{22}{\isachardoublequote}}}'' (repeat at least once), although
   this usually has a different operational behavior, such as solving
   goals in a different order.
 
   \medskip Iterated resolution, such as \verb|REPEAT (FIRSTGOAL|\isasep\isanewline%
 \verb|  (resolve_tac \<dots>))|, is usually better expressed using the \hyperlink{method.intro}{\mbox{\isa{intro}}} and \hyperlink{method.elim}{\mbox{\isa{elim}}} methods of Isar (see