diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2003-02-19 12:13:07 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2003-02-19 12:13:07 +0000 |
| commit | 9696feae2f1cab56a375a8881a3a9483fd5eb3c7 (patch) | |
| tree | 362b54d300dd201fdbbd2a08adc1197af1107f06 /isar | |
| parent | a6f7c0c9a31778993267c0ba4231d36ac2ae2a62 (diff) | |
Updated.
Diffstat (limited to 'isar')
| -rw-r--r-- | isar/todo | 6 |
1 files changed, 6 insertions, 0 deletions
@@ -4,6 +4,12 @@ See also ../todo for generic things to do, priority codes. +** B theorem dependencies: using Isar's "thm" command does not + work at top level. This is annoying for browsing the fully + qualified dependency names. (Even the ML_command "thm" + returns unknown theory context error). Can we use something + else? + ** B visualise dependencies: sometimes not applicable. ** C func-menu: observe proof-syntactic-context (general problem of |