[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!

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)]))






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.