doc-src/IsarRef/pure.tex
changeset 8195 af2575a5c5ae
parent 8101 ae555dd9585b
child 8207 985c876b777e
     1.1 --- a/doc-src/IsarRef/pure.tex	Fri Feb 04 21:53:36 2000 +0100
     1.2 +++ b/doc-src/IsarRef/pure.tex	Sat Feb 05 16:54:27 2000 +0100
     1.3 @@ -718,7 +718,7 @@
     1.4  \item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it
     1.5    abbreviates $\BY{default}$.
     1.6  \item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it
     1.7 -  abbreviates $\BY{assumption}$.
     1.8 +  abbreviates $\BY{this}$.
     1.9  \item [$\isarkeyword{sorry}$] is a \emph{fake proof}\index{proof!fake};
    1.10    provided that the \texttt{quick_and_dirty} flag is enabled,
    1.11    $\isarkeyword{sorry}$ pretends to solve the goal without further ado.  Of