-*- mode:outline -*-

* Things to do for Isabelle/Isar

See also ../todo for generic things to do, priority codes.

** 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);