doc-src/TutorialI/Documents/document/Documents.tex

 \ \ %
 \isamarkupcmt{(should not really bother)%
 }
 \isanewline
 \ \ \isamarkupfalse%
-\isacommand{by}\ {\isacharparenleft}rule\ impI{\isacharparenright}\ %
-\isamarkupcmt{implicit assumption step involved here%
-}
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent The above output has been produced as follows:
 

   is actually a fake:%
 \end{isamarkuptext}%
 \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:
 
 \begin{verbatim}