--- 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