--- a/doc-src/TutorialI/Types/Overloading0.thy Mon Mar 19 10:37:47 2001 +0100
+++ b/doc-src/TutorialI/Types/Overloading0.thy Mon Mar 19 12:38:36 2001 +0100
@@ -33,7 +33,7 @@
warnings to that effect.
However, there is nothing to prevent the user from forming terms such as
-@{text"inverse []"} and proving theorems as @{text"inverse []
+@{text"inverse []"} and proving theorems such as @{text"inverse []
= inverse []"}, although we never defined inverse on lists. We hasten to say
that there is nothing wrong with such terms and theorems. But it would be
nice if we could prevent their formation, simply because it is very likely