blob: 0adc6508e6d329ebabcc23e2ee06bc3288619d97 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
-*- mode:outline -*-
* Things to do for Isabelle/Isar
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
func-menu setup?);
** C undo 'use' command: unlock corresponding ML file;
** C provide template for empty theory (or even just for Scratch.thy);
** C proper proof-by-pointing support (hard; needs major reworking of
Isabelle's pretty-printing subsystem);
|