
diff -r 502a7c95de73 -r 342451d763f9 doc-src/TutorialI/Advanced/document/simp.tex
--- 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




