1.1 --- a/doc-src/Logics/LK.tex	Thu Feb 03 17:16:40 1994 +0100
     1.2 +++ b/doc-src/Logics/LK.tex	Fri Feb 04 10:32:27 1994 +0100
     1.3 @@ -272,12 +272,12 @@
     1.4  These tactics refine a subgoal into two by applying the cut rule.  The cut
     1.5  formula is given as a string, and replaces some other formula in the sequent.
     1.6  \begin{description}
     1.7 -\item[\ttindexbold{cutR_tac} {\it formula} {\it i}] 
     1.8 +\item[\ttindexbold{cutR_tac} {\it P\/} {\it i}] 
     1.9  reads an \LK{} formula~$P$, and applies the cut rule to subgoal~$i$.  It
    1.10  then deletes some formula from the right side of subgoal~$i$, replacing
    1.11  that formula by~$P$.
    1.12  
    1.13 -\item[\ttindexbold{cutL_tac} {\it formula} {\it i}] 
    1.14 +\item[\ttindexbold{cutL_tac} {\it P\/} {\it i}] 
    1.15  reads an \LK{} formula~$P$, and applies the cut rule to subgoal~$i$.  It
    1.16  then deletes some formula from the let side of the new subgoal $i+1$,
    1.17  replacing that formula by~$P$.