doc-src/IsarRef/conversion.tex

  Goalw [\(def@1\), \(\dots\)] "\(\phi\)";
 \end{ttbox}
 This may be replaced by using the $unfold$ proof method explicitly.
 \begin{matharray}{l}
 \LEMMA{name}{\texttt"{\phi}\texttt"} \\
-\quad \APPLY{unfold~def@1~\dots} \\
+\quad \APPLY{(unfold~def@1~\dots)} \\
 \end{matharray}
 
 
 \subsubsection{Deriving rules}
 

 new concept.  In that case, the general scheme for deriving rules may be
 greatly simplified, using one of the standard automated proof tools, such as
 $simp$, $blast$, or $auto$.  This could work as follows:
 \begin{matharray}{l}
   \LEMMA{}{\texttt"{\phi@1 \Imp \dots \Imp \psi}\texttt"} \\
-  \quad \BYY{unfold~defs}{blast} \\
+  \quad \BYY{(unfold~defs)}{blast} \\
 \end{matharray}
 Note that classic Isabelle would support this form only in the special case
 where $\phi@1$, \dots are atomic statements (when using the standard
 \texttt{Goal} command).  Otherwise the special treatment of rules would be
 applied, disturbing this simple setup.

 initial refinement step turn it into internal object-logic form using the
 $atomize$ method indicated below.  The remaining script is unchanged.
 
 \begin{matharray}{l}
   \LEMMA{name}{\texttt"{\All{\vec x}\vec\phi \Imp \psi}\texttt"} \\
-  \quad \APPLY{atomize~(full)} \\
+  \quad \APPLY{(atomize~(full))} \\
   \quad \APPLY{meth@1} \\
   \qquad \vdots \\
   \quad \DONE \\
 \end{matharray}