[isabelle] handy PG hack
Put the following code in your XEmacs init file, and you'll find that
C-c C-a C-t displays the theorem nearest the editor cursor ("point").
For GNU emacs, replace symbol-near-point by symbol-at-point.
Thanks to David Aspinall for this!
(eval-after-load "isar" ; bound to C-c C-a C-t
'(format "thm %s" (symbol-near-point))
This archive was generated by a fusion of
Pipermail (Mailman edition) and