diff -r f8da11ca4c6e -r 881222d48777 doc-src/TutorialI/todo.tobias
--- a/doc-src/TutorialI/todo.tobias	Mon Mar 12 18:23:11 2001 +0100
+++ b/doc-src/TutorialI/todo.tobias	Tue Mar 13 18:35:48 2001 +0100
@@ -61,14 +61,13 @@
 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
 Discrete math textbook: Rosen?
 
-say something about "abbreviations" when defs are introduced.
-
 adjust type of ^ in tab:overloading
 
 an example of induction: !y. A --> B --> C ??