1.1 --- a/doc-src/TutorialI/Advanced/document/simp.tex	Thu Jan 25 11:59:52 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Advanced/document/simp.tex	Thu Jan 25 15:31:31 2001 +0100
     1.3 @@ -94,8 +94,8 @@
     1.4  once they apply, they can be used forever. The simplifier is aware of this
     1.5  danger and treats permutative rules by means of a special strategy, called
     1.6  \bfindex{ordered rewriting}: a permutative rewrite
     1.7 -rule is only applied if the term becomes ``smaller'' (with respect to a fixed
     1.8 -lexicographic ordering on terms). For example, commutativity rewrites
     1.9 +rule is only applied if the term becomes smaller with respect to a fixed
    1.10 +lexicographic ordering on terms. For example, commutativity rewrites
    1.11  \isa{b\ {\isacharplus}\ a} to \isa{a\ {\isacharplus}\ b}, but then stops because \isa{a\ {\isacharplus}\ b} is strictly
    1.12  smaller than \isa{b\ {\isacharplus}\ a}.  Permutative rewrite rules can be turned into
    1.13  simplification rules in the usual manner via the \isa{simp} attribute; the
    1.14 @@ -150,7 +150,7 @@
    1.15  form (this will always be the case unless you have done something
    1.16  strange) where each occurrence of an unknown is of the form
    1.17  $\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound
    1.18 -variables. Thus all ``standard'' rewrite rules, where all unknowns are
    1.19 +variables. Thus all ordinary rewrite rules, where all unknowns are
    1.20  of base type, for example \isa{{\isacharquery}m\ {\isacharplus}\ {\isacharquery}n\ {\isacharplus}\ {\isacharquery}k\ {\isacharequal}\ {\isacharquery}m\ {\isacharplus}\ {\isacharparenleft}{\isacharquery}n\ {\isacharplus}\ {\isacharquery}k{\isacharparenright}}, are OK: if an unknown is
    1.21  of base type, it cannot have any arguments. Additionally, the rule
    1.22  \isa{{\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymand}\ {\isacharquery}Q\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}Q\ x{\isacharparenright}{\isacharparenright}} is also OK, in