--- a/doc-src/TutorialI/todo.tobias Wed Oct 11 00:03:22 2000 +0200
+++ b/doc-src/TutorialI/todo.tobias Wed Oct 11 09:09:06 2000 +0200
@@ -27,15 +27,16 @@
defs with = and pattern matching
-Why can't I declare trev at the end of Recdef/Nested0 and define it in
-Recdef/Nested1??
-
use arith_tac in recdef to solve termination conditions?
-> new example in Recdef/termination
a tactic for replacing a specific occurrence:
apply(substitute [2] thm)
+it would be nice if @term could deal with ?-vars.
+then a number of (unchecked!) @texts could be converted to @terms.
+
+
Minor fixes in the tutorial
===========================
@@ -45,8 +46,6 @@
Explain typographic conventions?
-how the simplifier works
-
an example of induction: !y. A --> B --> C ??
Advanced Ind expects rulify, mp and spec. How much really?
@@ -80,15 +79,18 @@
literature. In Recdef/termination.thy, at the end.
%FIXME, with one exception: nested recursion.
-Sets: rels and ^*
+Syntax section: syntax annotations nor just for consts but also for constdefs and datatype.
+
+Prove EU exercise in CTL.
Minor additions to the tutorial, unclear where
==============================================
-insert: lcp?
+Tacticals: , ? +
-Tacticals: , ? +
+"typedecl" is used in CTL/Base, but where is it introduced?
+In More Types chapter? Rephrase the CTL bit accordingly.
print_simpset (-> print_simps?)
(Another subsection Useful theorems, methods, and commands?)
@@ -107,7 +109,6 @@
demonstrate x : set xs in Sets. Or Tricks chapter?
-Table with symbols \<forall> etc. Apendix?
Appendix with HOL keywords. Say something about other keywords.
@@ -123,8 +124,6 @@
Nested inductive datatypes: another example/exercise:
size(t) <= size(subst s t)?
-Add Until to CTL.
-
insertion sort: primrec, later recdef
OTree: