doc-src/TutorialI/Misc/types.thy

--- a/doc-src/TutorialI/Misc/types.thy	Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/types.thy	Sun Aug 06 15:26:53 2000 +0200
@@ -30,7 +30,7 @@
 where \isacommand{defs}\indexbold{*defs} is a keyword and \isa{nand_def} and
 \isa{exor_def} are user-supplied names.
 The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
-that should only be used in constant definitions.
+that must be used in constant definitions.
 Declarations and definitions can also be merged
 *}