--- a/doc-src/IsarRef/pure.tex Mon Aug 23 15:24:00 1999 +0200
+++ b/doc-src/IsarRef/pure.tex Mon Aug 23 15:27:27 1999 +0200
@@ -659,8 +659,8 @@
Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done by simply
expanding the abbreviation by hand; note that $\PROOF{m@1}$ is usually
sufficient to see what is going wrong.
-\item [$\DDOT$] is a \emph{default proof}; it abbreviates $\BY{default}$.
-\item [$\DOT$] is a \emph{trivial proof}, it abbreviates $\BY{-}$, where
+\item [``$\DDOT$''] is a \emph{default proof}; it abbreviates $\BY{default}$.
+\item [``$\DOT$''] is a \emph{trivial proof}, it abbreviates $\BY{-}$, where
method ``$-$'' does nothing except inserting any facts into the proof state.
\item [$\isarkeyword{sorry}$] is a \emph{fake proof}; provided that
\texttt{quick_and_dirty} is enabled, $\isarkeyword{sorry}$ pretends to solve