diff options
author | 2001-12-04 16:16:00 +0000 | |
---|---|---|
committer | 2001-12-04 16:16:00 +0000 | |
commit | 125fadc2db026434af39c0694f8de198d4ed57fc (patch) | |
tree | d781b5bb3c0697846bb7a0ede3ffe3643fb9829c /doc | |
parent | dbcc799c6d2e7c2666389af109dd50ee19bf1c30 (diff) |
isar specific commands for bold/sup/sub;
Diffstat (limited to 'doc')
-rw-r--r-- | doc/ProofGeneral.texi | 20 |
1 files changed, 19 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 |