diff options
| -rw-r--r-- | doc/ProofGeneral.texi | 20 | ||||
| -rw-r--r-- | isar/isar.el | 10 |
2 files changed, 29 insertions, 1 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 0b5277ac..3575f480 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -2827,7 +2827,7 @@ next start Proof General. * The default value for XEmacs built for solaris is nil, because of unreliabilities with enablers there. -The default value is @code{t}. +The default value is @code{nil}. @end defopt @c This one removed: proof-auto-retract @@ -3710,6 +3710,24 @@ Shows all available commands of Isabelle/Isar's outer syntax. Shows theorems stored in the current theory node. @end table +@kindex C-c C-a b +@kindex C-c C-a u +@kindex C-c C-a l + +The following shortcuts insert control sequences into the text, +modifying the appearance of individual symbols (single letters, +mathematical entities etc.); the X-Symbol package will provide immediate +visual feedback. + +@table @kbd +@item C-c C-a b +Inserts "\<^bold>" +@item C-c C-a u +Inserts "\<^sup>" +@item C-c C-a l +Inserts "\<^sub>" +@end table + Command termination via `@code{;}' is an optional feature of Isar syntax. Neither Isabelle/Isar nor Proof General require semicolons to do their job. The following command allows to get rid of command diff --git a/isar/isar.el b/isar/isar.el index 56f7091c..db70761d 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -436,6 +436,16 @@ proof-shell-retract-files-regexp." ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Commands specific to isar ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(proof-defshortcut isar-bold "\\<^bold>" [(control b)]) +(proof-defshortcut isar-super "\\<^sup>" [(control u)]) +(proof-defshortcut isar-sub "\\<^sub>" [(control l)]) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Isar shell startup and exit hooks ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |