--- a/doc-src/TutorialI/todo.tobias Tue Dec 11 17:07:45 2001 +0100
+++ b/doc-src/TutorialI/todo.tobias Wed Dec 12 09:04:20 2001 +0100
@@ -36,9 +36,6 @@
use arith_tac in recdef to solve termination conditions?
-> new example in Recdef/termination
-a tactic for replacing a specific occurrence:
-apply(subst [2] thm)
-
it would be nice if @term could deal with ?-vars.
then a number of (unchecked!) @texts could be converted to @terms.
@@ -60,49 +57,16 @@
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.
-
-Advanced recdef: explain recdef_tc? No. Adjust recdef!
-
-Adjust FP textbook refs: new Bird, Hudak
-Discrete math textbook: Rosen?
-
-adjust type of ^ in tab:overloading
-
-an example of induction: !y. A --> B --> C ??
-
-Explain type_definition and mention pre-proved thms in subset.thy?
--> Types/typedef
-
Appendix: Lexical: long ids.
Warning: infixes automatically become reserved words!
-Forward ref from blast proof of Puzzle (AdvancedInd) to Isar proof?
-
-recdef with nested recursion: either an example or at least a pointer to the
-literature. In Recdef/termination.thy, at the end.
-%FIXME, with one exception: nested recursion.
-
Syntax section: syntax annotations not just for consts but also for constdefs and datatype.
Appendix with list functions.
All theory sources on the web?
-
-Minor additions to the tutorial, unclear where
-==============================================
-
-unfold?
-
-
Possible exercises
==================