--- a/doc-src/TutorialI/Recdef/document/Nested0.tex Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested0.tex Wed Aug 30 18:09:20 2000 +0200
@@ -13,9 +13,7 @@
you needed to reprove many lemmas reminiscent of similar lemmas about
\isa{rev}. We will now show you how \isacommand{recdef} can simplify
definitions and proofs about nested recursive datatypes. As an example we
-chose exercise~\ref{ex:trev-trev}:
-
-FIXME: declare trev now!%
+choose exercise~\ref{ex:trev-trev}:%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables: