doc-src/TutorialI/todo.tobias

--- a/doc-src/TutorialI/todo.tobias	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/todo.tobias	Wed Mar 07 15:54:11 2001 +0100
@@ -62,6 +62,8 @@
 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!
+
 warning: simp of asms from l to r; may require reordering (rotate_tac)
 
 Adjust FP textbook refs: new Bird, Hudak