--- a/doc-src/TutorialI/Recdef/Nested0.thy Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested0.thy Wed Aug 30 18:09:20 2000 +0200
@@ -15,9 +15,7 @@
you needed to reprove many lemmas reminiscent of similar lemmas about
@{term"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}:
*}
(* consts trev :: "('a,'b)term => ('a,'b)term" *)
(*<*)