Email Gateway (Aug 17 2022 at 13:45): Email Gateway (Aug 17 2022 at 13:45):From: Lawrence Paulson <lp15@cam.ac.uk>
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!
Larry
(eval-after-load "isar" ; bound to C-c C-a C-t
'(proof-definvisible isar-theorem-at-point
'(format "thm %s" (symbol-near-point))
[(control t)]))
Last updated: May 03 2024 at 08:18 UTC