# HG changeset patch
# User wenzelm
# Date 1011025902 -3600
# Node ID 147e0137a76a8fd358d23ff3555d9a10e017df8f
# Parent  c0ce43e809fd26772716bd5a924e59ddba5eb8a7
tuned;

diff -r c0ce43e809fd -r 147e0137a76a doc-src/TutorialI/Documents/Documents.thy
--- a/doc-src/TutorialI/Documents/Documents.thy	Mon Jan 14 17:29:25 2002 +0100
+++ b/doc-src/TutorialI/Documents/Documents.thy	Mon Jan 14 17:31:42 2002 +0100
@@ -805,9 +805,8 @@
   elements need to be kept in mind, too --- the system performs little
   sanity checks here.  Arguments of markup commands and formal
   comments must not be hidden, otherwise presentation fails.  Open and
-  close parentheses need to be inserted carefully; it is fairly easy
-  to hide the wrong parts, especially after rearranging the theory
-  text.
+  close parentheses need to be inserted carefully; it is easy to hide
+  the wrong parts, especially after rearranging the theory text.
 *}
 
 (*<*)