--- a/doc-src/TutorialI/Rules/document/find2.tex Sun Aug 28 19:42:10 2005 +0200
+++ b/doc-src/TutorialI/Rules/document/find2.tex Sun Aug 28 19:42:19 2005 +0200
@@ -7,6 +7,7 @@
\endisadelimtheory
%
\isatagtheory
+\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
@@ -14,13 +15,13 @@
\isadelimtheory
%
\endisadelimtheory
+\isamarkupfalse%
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
-\isamarkuptrue%
%
\begin{isamarkuptxt}%
\index{finding theorems}\index{searching theorems} In
@@ -40,6 +41,8 @@
the very theorem you are trying to prove is already in the
database. Given the goal%
\end{isamarkuptxt}%
+\isamarkuptrue%
+\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
@@ -47,13 +50,13 @@
\isadelimproof
%
\endisadelimproof
+\isamarkupfalse%
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
-\isamarkuptrue%
%
\begin{isamarkuptxt}%
\vspace{-\bigskipamount}
@@ -74,6 +77,8 @@
\texttt{dest} is analogous to \texttt{intro} but takes the assumptions
into account, too.%
\end{isamarkuptxt}%
+\isamarkuptrue%
+\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
@@ -87,6 +92,7 @@
\endisadelimtheory
%
\isatagtheory
+\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%