diff -r bb01189f0565 -r 67cec35dbc58 doc-src/TutorialI/todo.tobias
--- a/doc-src/TutorialI/todo.tobias	Wed Mar 14 08:50:55 2001 +0100
+++ b/doc-src/TutorialI/todo.tobias	Wed Mar 14 17:38:49 2001 +0100
@@ -57,12 +57,6 @@
 
 Advanced recdef: explain recdef_tc?
 
-I guess we should say "HOL" everywhere, with a remark early on about the
-differences between our HOL and the other one.
-
-Syntax translations! Harpoons already used!
-say something about "abbreviations" when defs are introduced.
-
 warning: simp of asms from l to r; may require reordering (rotate_tac)
 
 Adjust FP textbook refs: new Bird, Hudak