diff -r 2626d4e37341 -r 9554ce1c2e54 doc-src/TutorialI/todo.tobias
--- a/doc-src/TutorialI/todo.tobias	Thu Oct 19 21:25:15 2000 +0200
+++ b/doc-src/TutorialI/todo.tobias	Fri Oct 20 08:46:41 2000 +0200
@@ -1,27 +1,21 @@
-General questions
-=================
-
-Here is an initial list:
-clarify, clarsimp, hyp_subst_tac, rename_tac, rotate_tac, split
-single step tactics: (e/d/f)rule, insert
-with instantiation: (e/d/f)rule_tac, insert_tac
+Implementation
+==============
 
 Hide global names like Node.
 Why is comp needed in addition to op O?
 Explain in syntax section!
 
-Implementation
-==============
+defs with = and pattern matching
 
-swap in classical.ML has ugly name Pa in it. Rename.
+replace "simp only split" by "split_tac".
 
-Induction rules for int: int_le/ge_induct?
-Needed for ifak example. But is that example worth it?
+arithmetic: allow mixed nat/int formulae
+-> simplify proof of part1 in Inductive/AB.thy
 
 Add map_cong?? (upto 10% slower)
-But we should install UN_cong and INT_cong too.
 
-defs with = and pattern matching
+Recdef: Get rid of function name in header.
+Support mutual recursion (Konrad?)
 
 use arith_tac in recdef to solve termination conditions?
 -> new example in Recdef/termination
@@ -34,15 +28,18 @@
 
 it would be nice if one could get id to the enclosing quotes in the [source] option.
 
-arithmetic: allow mixed nat/int formulae
--> simplify proof of part1 in Inductive/AB.thy
+More predefined functions for datatypes: map?
+
+Induction rules for int: int_le/ge_induct?
+Needed for ifak example. But is that example worth it?
+
 
 Minor fixes in the tutorial
 ===========================
 
-replace simp only split by split_tac.
+explanation of absence of contrapos_pn in Rules?
 
-get rid of use_thy?
+get rid of use_thy in tutorial?
 
 Explain typographic conventions?
 
@@ -62,27 +59,19 @@
 
 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
 ==============================================
 
 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?)
-
 Mention that simp etc (big step tactics) insist on change?
 
 Rules: Introduce "by" (as a kind of shorthand for apply+done, except that it
 does more.)
 
 A list of further useful commands (rules? tricks?)
-prefer, defer
+prefer, defer, print_simpset (-> print_simps?)
 
 An overview of the automatic methods: simp, auto, fast, blast, force,
 clarify, clarsimp (intro, elim?)
@@ -134,12 +123,8 @@
 
 Sets via ordered list of intervals. (Isa/Interval(2))
 
-Sets: PDL and CTL
-
-Ind. defs: Grammar (for same number of as and bs),
 propositional logic (soundness and completeness?),
 predicate logic (soundness?),
-CTL proof.
 
 Tautology checker. Based on Ifexpr or prop.logic?
 Include forward reference in relevant section.
@@ -159,33 +144,18 @@
 Additional topics
 =================
 
-Beef up recdef (see below).
-Nested recursion? Mutual recursion?
-
-Nested inductive datatypes: better recursion and induction
-(see below)
+Recdef with nested recursion?
 
 Extensionality: applications in
 - boolean expressions: valif o bool2if = value
 - Advanced datatypes exercise subst (f o g) = subst f o subst g
 
 A look at the library?
-Functions. Relations. Lfp/Gfp. Map.
+Map.
 If WF is discussed, make a link to it from AdvancedInd.
 
 Prototyping?
 
-
-Isabelle
-========
-
-Get rid of function name in recdef header
-
-More predefined functions for datatypes: map?
-
-1 and 2 on nat?
-
-
 ==============================================================
 Recdef: