# HG changeset patch
# User nipkow
# Date 988905089 -7200
# Node ID 297a58ea405f76e1b8bec5f907b94b1170084b9b
# Parent  f2a284b2d5887d18a7ab6b9322831d6b96f94858
*** empty log message ***

diff -r f2a284b2d588 -r 297a58ea405f doc-src/TutorialI/todo.tobias
--- a/doc-src/TutorialI/todo.tobias	Thu May 03 11:53:42 2001 +0200
+++ b/doc-src/TutorialI/todo.tobias	Thu May 03 17:51:29 2001 +0200
@@ -26,6 +26,11 @@
 Recdef: Get rid of function name in header.
 Support mutual recursion (Konrad?)
 
+improve solver in simplifier: treat & and ! ...
+
+better 1 point rules:
+!x. !y. x = f y --> P x y  should reduce to  !y. P (f y) y.
+
 use arith_tac in recdef to solve termination conditions?
 -> new example in Recdef/termination
 
@@ -53,7 +58,7 @@
 Minor fixes in the tutorial
 ===========================
 
-recdef: failed tcs no longer shown!
+recdef: failed tcs no longer shown! (sec:Recursion over nested datatypes)
 say something about how conditions are proved?
 No, better show failed proof attempts.