| changeset 10236 | 7626cb4e1407 |
| parent 10217 | e61e7e1eacaf |
| child 10237 | 875bf54b5d74 |
--- a/doc-src/TutorialI/todo.tobias Tue Oct 17 10:45:51 2000 +0200 +++ b/doc-src/TutorialI/todo.tobias Tue Oct 17 13:28:57 2000 +0200 @@ -36,6 +36,8 @@ 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 Minor fixes in the tutorial ===========================