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

author | lcp |

Wed, 03 May 1995 16:10:41 +0200 | |

changeset 1100 | 74921c7613e7 |

parent 1099 | f4335b56f772 |

child 1101 | b9594fe65d89 |

trivial change

--- 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: