| changeset 13024 | 0461b281c2b5 |
| parent 13013 | 4db07fc3d96f |
| child 13041 | 6faccf7d0f25 |
--- a/doc-src/IsarRef/conversion.tex Tue Mar 05 18:54:55 2002 +0100 +++ b/doc-src/IsarRef/conversion.tex Tue Mar 05 18:55:46 2002 +0100 @@ -221,7 +221,7 @@ $simp$, $blast$, or $auto$. This would work as follows: \begin{matharray}{l} \LEMMA{}{\texttt"{\phi@1 \Imp \dots \Imp \psi}\texttt"} \\ - \quad \APPLY{unfold~defs} \quad \CMT{or ``$\APPLY{insert~facts}$''} \\ + \quad \APPLY{unfold~defs} \\ \quad \APPLY{blast} \\ \quad \DONE \\ \end{matharray}