doc-src/TutorialI/todo.tobias
changeset 11561 6a95f3eaa54f
parent 11548 0028bd06a19c
child 12328 7c4ec77a8715
     1.1 --- a/doc-src/TutorialI/todo.tobias	Mon Sep 10 18:31:24 2001 +0200
     1.2 +++ b/doc-src/TutorialI/todo.tobias	Tue Sep 11 15:36:16 2001 +0200
     1.3 @@ -60,6 +60,10 @@
     1.4  Minor fixes in the tutorial
     1.5  ===========================
     1.6  
     1.7 +1/2 no longer abbrevs for Suc.
     1.8 +Warning: needs simplification to turn 1 into Suc 0. arith does so
     1.9 +automatically.
    1.10 +
    1.11  recdef: failed tcs no longer shown! (sec:Recursion over nested datatypes)
    1.12  say something about how conditions are proved?
    1.13  No, better show failed proof attempts.