1.1 --- a/doc-src/TutorialI/todo.tobias	Thu Dec 13 16:48:07 2001 +0100
     1.2 +++ b/doc-src/TutorialI/todo.tobias	Thu Dec 13 16:48:34 2001 +0100
     1.3 @@ -3,28 +3,10 @@
     1.4  Implementation
     1.5  ==============
     1.6  
     1.7 -- (#2 * x) = #2 * - x is not proved by arith
     1.8 +Add map_cong?? (upto 10% slower)
     1.9  
    1.10  a simp command for terms
    1.11  
    1.12 -----------------------------------------------------------------------
    1.13 -primrec 
    1.14 -"(foorec [] []) = []"
    1.15 -"(foorec [] (y # ys)) = (y # (foorec [] ys))"
    1.16 -
    1.17 -*** Primrec definition error:
    1.18 -*** extra variables on rhs: "y", "ys"
    1.19 -*** in
    1.20 -*** "((foorec [] ((y::'a_1) # (ys::'a_1 list))) = (y # (foorec [] ys)))"
    1.21 -*** At command "primrec".
    1.22 -
    1.23 -Bessere Fehlermeldung!
    1.24 -----------------------------------------------------------------------
    1.25 -
    1.26 -Relation: comp -> composition
    1.27 -
    1.28 -Add map_cong?? (upto 10% slower)
    1.29 -
    1.30  Recdef: Get rid of function name in header.
    1.31  Support mutual recursion (Konrad?)
    1.32  
    1.33 @@ -33,9 +15,6 @@
    1.34  better 1 point rules:
    1.35  !x. !y. x = f y --> P x y  should reduce to  !y. P (f y) y.
    1.36  
    1.37 -use arith_tac in recdef to solve termination conditions?
    1.38 --> new example in Recdef/termination
    1.39 -
    1.40  it would be nice if @term could deal with ?-vars.
    1.41  then a number of (unchecked!) @texts could be converted to @terms.
    1.42