--- 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: