# HG changeset patch
# User lcp
# Date 760354347 -3600
# Node ID ca6eb7e6e94f74c7577883db39e03f35d727e832
# Parent  d45f0af592f02aa9fe9043dd70fa04ecc48e661e
correction to cut tactics

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