diff -r cb3612cc41a3 -r fc075ae929e4 doc-src/TutorialI/Documents/document/Documents.tex
--- a/doc-src/TutorialI/Documents/document/Documents.tex	Sun Jan 30 20:48:50 2005 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Tue Feb 01 18:01:57 2005 +0100
@@ -587,9 +587,6 @@
 }
 \isanewline
 \ \ \isamarkupfalse%
-\isacommand{by}\ {\isacharparenleft}rule\ impI{\isacharparenright}\ %
-\isamarkupcmt{implicit assumption step involved here%
-}
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%
@@ -815,7 +812,7 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}x\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isacharless}\ x\ {\isacharasterisk}\ x{\isachardoublequote}\isanewline
 \ \ \isamarkupfalse%
-\isacommand{by}\ {\isacharparenleft}auto{\isacharparenright}\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent Here the real source of the proof has been as follows: