# HG changeset patch
# User lcp
# Date 799510241 -7200
# Node ID 74921c7613e7b9627587e769e0313ba0b5fe8f2b
# Parent  f4335b56f7723ab32865ba7cf41fd7a8faebd570
trivial change

diff -r f4335b56f772 -r 74921c7613e7 doc-src/Ref/simp.tex
--- 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: