doc-src/TutorialI/todo.tobias

--- a/doc-src/TutorialI/todo.tobias	Fri Mar 09 19:05:48 2001 +0100
+++ b/doc-src/TutorialI/todo.tobias	Mon Mar 12 18:17:45 2001 +0100
@@ -57,8 +57,6 @@
 
 Advanced recdef: explain recdef_tc?
 
-say something about definitional approach. In recdef section? At the end?
-
 I guess we should say "HOL" everywhere, with a remark early on about the
 differences between our HOL and the other one.