diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Advanced/document/simp.tex
--- a/doc-src/TutorialI/Advanced/document/simp.tex	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Advanced/document/simp.tex	Fri Jan 05 18:32:57 2001 +0100
@@ -93,7 +93,7 @@
 once they apply, they can be used forever. The simplifier is aware of this
 danger and treats permutative rules by means of a special strategy, called
 \bfindex{ordered rewriting}: a permutative rewrite
-rule is only applied if the term becomes ``smaller'' (w.r.t.\ some fixed
+rule is only applied if the term becomes ``smaller'' (with respect to a fixed
 lexicographic ordering on terms). For example, commutativity rewrites
 \isa{b\ {\isacharplus}\ a} to \isa{a\ {\isacharplus}\ b}, but then stops because \isa{a\ {\isacharplus}\ b} is strictly
 smaller than \isa{b\ {\isacharplus}\ a}.  Permutative rewrite rules can be turned into