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