diff -r eacce1cd716a -r 05fc32a23b8b doc-src/TutorialI/Rules/document/find2.tex
--- a/doc-src/TutorialI/Rules/document/find2.tex	Tue Aug 16 13:42:21 2005 +0200
+++ b/doc-src/TutorialI/Rules/document/find2.tex	Tue Aug 16 13:42:23 2005 +0200
@@ -1,8 +1,26 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{find{\isadigit{2}}}%
-\isamarkupfalse%
-\isamarkupfalse%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isamarkuptrue%
 %
 \begin{isamarkuptxt}%
 \index{finding theorems}\index{searching theorems} In
@@ -22,9 +40,20 @@
 the very theorem you are trying to prove is already in the
 database.  Given the goal%
 \end{isamarkuptxt}%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
 \isamarkuptrue%
-\isamarkupfalse%
-\isamarkupfalse%
 %
 \begin{isamarkuptxt}%
 \vspace{-\bigskipamount}
@@ -45,9 +74,26 @@
 \texttt{dest} is analogous to \texttt{intro} but takes the assumptions
 into account, too.%
 \end{isamarkuptxt}%
-\isamarkuptrue%
-\isamarkupfalse%
-\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex