author | nipkow |
Tue, 11 Sep 2001 15:36:16 +0200 | |
changeset 11561 | 6a95f3eaa54f |
parent 11560 | 46d0bde121ab |
child 11562 | 804ee65ee1a1 |
--- a/doc-src/TutorialI/todo.tobias Mon Sep 10 18:31:24 2001 +0200 +++ b/doc-src/TutorialI/todo.tobias Tue Sep 11 15:36:16 2001 +0200 @@ -60,6 +60,10 @@ Minor fixes in the tutorial =========================== +1/2 no longer abbrevs for Suc. +Warning: needs simplification to turn 1 into Suc 0. arith does so +automatically. + recdef: failed tcs no longer shown! (sec:Recursion over nested datatypes) say something about how conditions are proved? No, better show failed proof attempts.