diff -r ecb6eaa76843 -r 0a380ac80e7d doc-src/TutorialI/todo.tobias
--- a/doc-src/TutorialI/todo.tobias	Thu Oct 26 09:15:59 2000 +0200
+++ b/doc-src/TutorialI/todo.tobias	Thu Oct 26 10:27:04 2000 +0200
@@ -5,8 +5,6 @@
 Why is comp needed in addition to op O?
 Explain in syntax section!
 
-defs with = and pattern matching
-
 replace "simp only split" by "split_tac".
 
 arithmetic: allow mixed nat/int formulae
@@ -33,11 +31,17 @@
 Induction rules for int: int_le/ge_induct?
 Needed for ifak example. But is that example worth it?
 
+defs with = and pattern matching
+
 
 Minor fixes in the tutorial
 ===========================
 
-explanation of absence of contrapos_pn in Rules?
+explanation of term "contrapositive"/contraposition in Rules?
+Index the notion and maybe the rules contrapos_xy
+
+Even: forward ref from problem with "Suc(Suc n) : even" to general solution in
+AdvancedInd section.
 
 get rid of use_thy in tutorial?