--- a/doc-src/TutorialI/Documents/document/Documents.tex Wed May 25 09:03:53 2005 +0200
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Wed May 25 09:04:24 2005 +0200
@@ -587,6 +587,9 @@
}
\isanewline
\ \ \isamarkupfalse%
+\isacommand{by}\ {\isacharparenleft}rule\ impI{\isacharparenright}\ %
+\isamarkupcmt{implicit assumption step involved here%
+}
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -812,7 +815,7 @@
\isamarkuptrue%
\isacommand{lemma}\ {\isachardoublequote}x\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isacharless}\ x\ {\isacharasterisk}\ x{\isachardoublequote}\isanewline
\ \ \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{by}\ {\isacharparenleft}auto{\isacharparenright}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent Here the real source of the proof has been as follows: