--- a/doc-src/TutorialI/Advanced/document/simp.tex Fri Nov 28 12:09:37 2003 +0100
+++ b/doc-src/TutorialI/Advanced/document/simp.tex Tue Dec 02 11:48:15 2003 +0100
@@ -160,7 +160,7 @@
Each occurrence of an unknown is of the form
$\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound
variables. Thus all ordinary rewrite rules, where all unknowns are
-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 acceptable: if an unknown is
+of base type, for example \isa{{\isacharquery}a\ {\isacharplus}\ {\isacharquery}b\ {\isacharplus}\ {\isacharquery}c\ {\isacharequal}\ {\isacharquery}a\ {\isacharplus}\ {\isacharparenleft}{\isacharquery}b\ {\isacharplus}\ {\isacharquery}c{\isacharparenright}}, are acceptable: if an unknown is
of base type, it cannot have any arguments. Additionally, the rule
\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 acceptable, in
both directions: all arguments of the unknowns \isa{{\isacharquery}P} and