diff -r 11aa41ed306d -r 1eced27ee0e1 doc-src/TutorialI/Rules/document/find2.tex --- 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}%