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