Email Gateway (Aug 18 2022 at 11:17): Email Gateway (Aug 18 2022 at 11:17):From: "Mark A. Hillebrand" <mah@dfki.de>
Hi,
Actually there isn't one predefined for ML{* *}; the place to define
that would supposedly be near
(proof-defshortcut isar-antiquote "@{text \"%p\"}" [(control a)])
in ProofGeneral's isar/isar.el file.
When looking for documentation for the antiquotation key bindings, I
noticed that the PG general documentation for the special Isar keys is
slightly out of sync (and also doesn't list the C-c C-a C-a key
binding).
Attached to this mail is a patch for ProofGeneral's
doc/ProofGeneral.texi (against version 3.7pre080117), which hopefully
fixes the out-of-sync doc. (Yes, I will upload that to the PG Wiki).
Best regards,
Mark
ProofGeneral_isar_keybinding_docfix.texi.diff
Last updated: May 03 2024 at 12:27 UTC