1.1 --- a/doc-src/IsarRef/generic.tex	Thu Mar 07 22:52:07 2002 +0100
     1.2 +++ b/doc-src/IsarRef/generic.tex	Thu Mar 07 23:21:19 2002 +0100
     1.3 @@ -230,8 +230,8 @@
     1.4    \quad \PROOF{succeed} \\
     1.5    \qquad \FIX{thesis} \\
     1.6    \qquad \ASSUME{that~[intro?]}{\All{\vec x} \vec\phi \Imp thesis} \\
     1.7 -  \qquad \SHOW{}{thesis} \\
     1.8 -  \quad\qquad \APPLY{insert~that} \\
     1.9 +  \qquad \THUS{}{thesis} \\
    1.10 +  \quad\qquad \APPLY{-} \\
    1.11    \quad\qquad \USING{\vec b}~~\langle proof\rangle \\
    1.12    \quad \QED{} \\
    1.13    \quad \FIX{\vec x}~\ASSUMENAME^\ast~a\colon~\vec\phi \\