--- a/doc-src/IsarRef/conversion.tex Thu Mar 07 22:52:07 2002 +0100
+++ b/doc-src/IsarRef/conversion.tex Thu Mar 07 23:21:19 2002 +0100
@@ -188,7 +188,7 @@
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}
@@ -224,7 +224,7 @@
$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
@@ -265,7 +265,7 @@
\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 \\