diff -r 65ede8dfe304 -r bb4ede27fcb7 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