diff -r e928bdf62014 -r e61e7e1eacaf doc-src/TutorialI/todo.tobias
--- a/doc-src/TutorialI/todo.tobias	Fri Oct 13 11:15:56 2000 +0200
+++ b/doc-src/TutorialI/todo.tobias	Fri Oct 13 18:02:08 2000 +0200
@@ -48,7 +48,8 @@
 
 an example of induction: !y. A --> B --> C ??
 
-Advanced Ind expects rulify, mp and spec. How much really?
+Advanced Ind expects rule_format incl (no_asm) (which it currently explains!
+Where explained?
 
 Appendix: Lexical: long ids.
 
@@ -58,9 +59,6 @@
 
 mention split_split in advanced pair section.
 
-Advanced:
-rule induction where premise not atomic (x1...xn) : R.
-
 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.