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

doc-src/Ref/simp.tex

changeset 1100 | 74921c7613e7 |

parent 323 | 361a71713176 |

child 9695 | ec7d7f877712 |

--- a/doc-src/Ref/simp.tex Wed May 03 15:33:40 1995 +0200 +++ b/doc-src/Ref/simp.tex Wed May 03 16:10:41 1995 +0200 @@ -55,7 +55,7 @@ \Imp (\Var{P@1} \imp \Var{P@2}) \bimp (\Var{Q@1} \imp \Var{Q@2}) \] This rule assumes $Q@1$, and any rewrite rules it contains, while -simplifying~$P@2$. Such ``local'' assumptions are effective for rewriting +simplifying~$P@2$. Such `local' assumptions are effective for rewriting formulae such as $x=0\imp y+x=y$. {\bf Additional quantifiers} are allowed, typically for binding operators: