summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/Logics/LK.tex

changeset 264 | ca6eb7e6e94f |

parent 111 | 1b3cddf41b2d |

child 291 | a615050a7494 |

--- 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$.