summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | lcp |

Fri, 04 Feb 1994 10:32:27 +0100 | |

changeset 264 | ca6eb7e6e94f |

parent 263 | d45f0af592f0 |

child 265 | 443dc2c37583 |

correction to cut tactics

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