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