blob: 944083dc3d742b296c37f9f74716b7eb170f7504 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
-*- mode:outline -*-
* Things to do for Isabelle/Isar
See also ../todo for generic things to do, priority codes.
** 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);
** C speedup indentation (rather do this at generic level?); would be
nice if current indentation stack would be somehow stored within the
extend(s) processed last;
** C tune behaviour of goals/response buffers (e.g. hide empty
response buffers when using 2 buffer model);
** C eliminate x-symbol-isar.el in favour of shared x-symbol-isabelle.el;
** D Combine with isa/ to get single Isabelle PG instance, somehow?
Then users could use both proof languages in the same session.
|
