--- a/doc-src/TutorialI/Types/document/Overloading0.tex Fri May 18 17:18:43 2001 +0200
+++ b/doc-src/TutorialI/Types/document/Overloading0.tex Sat May 19 12:19:23 2001 +0200
@@ -33,7 +33,7 @@
left it is \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} but on the right \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} and
\isa{{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}. The annotation \isa{{\isacharparenleft}}\isacommand{overloaded}\isa{{\isacharparenright}} tells Isabelle that
the definitions do intentionally define \isa{inverse} only at
-instances of its declared type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely supresses
+instances of its declared type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely suppresses
warnings to that effect.
However, there is nothing to prevent the user from forming terms such as