diff -r 352f6f209775 -r 620647438780 doc-src/TutorialI/todo.tobias
--- a/doc-src/TutorialI/todo.tobias	Wed Dec 06 12:34:40 2000 +0100
+++ b/doc-src/TutorialI/todo.tobias	Wed Dec 06 13:22:58 2000 +0100
@@ -1,14 +1,10 @@
 Implementation
 ==============
 
-Why is comp needed in addition to op O?
-Explain in syntax section!
+Relation: comp -> composition
 
 replace "simp only split" by "split_tac".
 
-arithmetic: allow mixed nat/int formulae
--> simplify proof of part1 in Inductive/AB.thy
-
 Add map_cong?? (upto 10% slower)
 
 Recdef: Get rid of function name in header.
@@ -30,6 +26,9 @@
 Induction rules for int: int_le/ge_induct?
 Needed for ifak example. But is that example worth it?
 
+Komischerweise geht das Splitten von _Annahmen_ auch mit simp_tac, was
+ein generelles Feature ist, das man vielleicht mal abstellen sollte.
+
 proper mutual simplification
 
 defs with = and pattern matching??
@@ -62,8 +61,6 @@
 
 Forward ref from blast proof of Puzzle (AdvancedInd) to Isar proof?
 
-mention split_split in advanced pair section.
-
 recdef with nested recursion: either an example or at least a pointer to the
 literature. In Recdef/termination.thy, at the end.
 %FIXME, with one exception: nested recursion.