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