--- a/doc-src/TutorialI/todo.tobias Sat Feb 17 10:43:53 2001 +0100
+++ b/doc-src/TutorialI/todo.tobias Tue Feb 20 10:18:26 2001 +0100
@@ -1,6 +1,8 @@
Implementation
==============
+- (#2 * x) = #2 * - x is not proved by arith
+
Relation: comp -> composition
Add map_cong?? (upto 10% slower)
@@ -35,6 +37,9 @@
Minor fixes in the tutorial
===========================
+I guess we should say "HOL" everywhere, with a remark early on about the
+differences between our HOL and the other one.
+
warning: simp of asms from l to r; may require reordering (rotate_tac)
Adjust FP textbook refs: new Bird, Hudak