doc-src/TutorialI/todo.tobias
changeset 10236 7626cb4e1407
parent 10217 e61e7e1eacaf
child 10237 875bf54b5d74
     1.1 --- a/doc-src/TutorialI/todo.tobias	Tue Oct 17 10:45:51 2000 +0200
     1.2 +++ b/doc-src/TutorialI/todo.tobias	Tue Oct 17 13:28:57 2000 +0200
     1.3 @@ -36,6 +36,8 @@
     1.4  
     1.5  it would be nice if one could get id to the enclosing quotes in the [source] option.
     1.6  
     1.7 +arithmetic: allow mixed nat/int formulae
     1.8 +-> simplify proof of part1 in Inductive/AB.thy
     1.9  
    1.10  Minor fixes in the tutorial
    1.11  ===========================