*** empty log message ***
authornipkow
Tue, 11 Sep 2001 15:36:16 +0200
changeset 11561 6a95f3eaa54f
parent 11560 46d0bde121ab
child 11562 804ee65ee1a1
*** empty log message ***
doc-src/TutorialI/todo.tobias
--- 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.