1.1 --- a/doc-src/TutorialI/todo.tobias	Wed Oct 11 00:03:22 2000 +0200
     1.2 +++ b/doc-src/TutorialI/todo.tobias	Wed Oct 11 09:09:06 2000 +0200
     1.3 @@ -27,15 +27,16 @@
     1.4  
     1.5  defs with = and pattern matching
     1.6  
     1.7 -Why can't I declare trev at the end of Recdef/Nested0 and define it in
     1.8 -Recdef/Nested1??
     1.9 -
    1.10  use arith_tac in recdef to solve termination conditions?
    1.11  -> new example in Recdef/termination
    1.12  
    1.13  a tactic for replacing a specific occurrence:
    1.14  apply(substitute [2] thm)
    1.15  
    1.16 +it would be nice if @term could deal with ?-vars.
    1.17 +then a number of (unchecked!) @texts could be converted to @terms.
    1.18 +
    1.19 +
    1.20  Minor fixes in the tutorial
    1.21  ===========================
    1.22  
    1.23 @@ -45,8 +46,6 @@
    1.24  
    1.25  Explain typographic conventions?
    1.26  
    1.27 -how the simplifier works
    1.28 -
    1.29  an example of induction: !y. A --> B --> C ??
    1.30  
    1.31  Advanced Ind expects rulify, mp and spec. How much really?
    1.32 @@ -80,15 +79,18 @@
    1.33  literature. In Recdef/termination.thy, at the end.
    1.34  %FIXME, with one exception: nested recursion.
    1.35  
    1.36 -Sets: rels and ^*
    1.37 +Syntax section: syntax annotations nor just for consts but also for constdefs and datatype.
    1.38 +
    1.39 +Prove EU exercise in CTL.
    1.40  
    1.41  
    1.42  Minor additions to the tutorial, unclear where
    1.43  ==============================================
    1.44  
    1.45 -insert: lcp?
    1.46 +Tacticals: , ? +
    1.47  
    1.48 -Tacticals: , ? +
    1.49 +"typedecl" is used in CTL/Base, but where is it introduced?
    1.50 +In More Types chapter? Rephrase the CTL bit accordingly.
    1.51  
    1.52  print_simpset (-> print_simps?)
    1.53  (Another subsection Useful theorems, methods, and commands?)
    1.54 @@ -107,7 +109,6 @@
    1.55  
    1.56  demonstrate x : set xs in Sets. Or Tricks chapter?
    1.57  
    1.58 -Table with symbols \<forall> etc. Apendix?
    1.59  Appendix with HOL keywords. Say something about other keywords.
    1.60  
    1.61  
    1.62 @@ -123,8 +124,6 @@
    1.63  Nested inductive datatypes: another example/exercise:
    1.64   size(t) <= size(subst s t)?
    1.65  
    1.66 -Add Until to CTL.
    1.67 -
    1.68  insertion sort: primrec, later recdef
    1.69  
    1.70  OTree: