Ticket #171: ProofGeneral_isar_keybinding_docfix.texi.diff

File ProofGeneral_isar_keybinding_docfix.texi.diff, 2.1 KB (added by Mark A. Hillebrand, 16 years ago)

  • ProofGeneral.texi

    old new  
    36603660@kindex C-c C-a r
    36613661@kindex C-c C-a C-q
    36623662@kindex C-c C-a C-d
     3663@kindex C-c C-a C-p
    36633664@kindex C-c C-a h A
    36643665@kindex C-c C-a h C
    36653666@kindex C-c C-a h I
    … …  
    36733674@kindex C-c C-a h m
    36743675@kindex C-c C-a h o
    36753676@kindex C-c C-a h t
     3677@kindex C-c C-a C-s
    36763678
    36773679The Isabelle instance of Proof General supplies several specific
    36783680help key bindings; these functions are offered within the prover help
    … …  
    36863688Invokes @code{quickcheck} on the current subgoal.
    36873689@item C-c C-a C-d
    36883690Displays a draft document of the current theory.
     3691@item C-c C-a C-p
     3692Prints a draft document of the current theory.
    36893693@item C-c C-a h A
    36903694Shows available antiquotation commands and options.
    36913695@item C-c C-a h C
    … …  
    37123716Shows all available commands of Isabelle's outer syntax.
    37133717@item C-c C-a h t
    37143718Shows theorems stored in the current theory node.
     3719@item C-c C-a C-s
     3720Invoke sledgehammer on first subgoal.
    37153721@end table
    37163722
    3717 @c @kindex C-c C-a b
     3723@kindex C-c C-a b
     3724@kindex C-c C-a C-b
     3725@kindex C-c C-a C-u
     3726@kindex C-c C-a C-l
    37183727@kindex C-c C-a u
    37193728@kindex C-c C-a l
    3720 @kindex C-c C-a i
    3721 @kindex C-c C-a C-l
    3722 @kindex C-c C-a C-u
    3723 @kindex C-c C-a C-w
     3729@kindex C-c C-a C-i
     3730@kindex C-c C-a C-r
     3731@kindex C-c C-a C-a
    37243732
    37253733The following shortcuts insert control sequences into the text,
    37263734modifying the appearance of individual symbols (single letters,
    … …  
    37283736visual feedback.
    37293737
    37303738@table @kbd
    3731 @c @item C-c C-a b
    3732 @c Inserts "\<^bold>"
     3739@item C-c C-a b
     3740Inserts "\<^bold>"
     3741@item C-c C-a C-b
     3742Inserts "\<^loc>"
    37333743@item C-c C-a C-u
    37343744Inserts "\<^sup>"  (superscript character)
    37353745@item C-c C-a C-l
    … …  
    37403750Inserts "\<^bsub> \<^esub>"  (subscript string)
    37413751@item C-c C-a C-i
    37423752Inserts "\<^isub>"  (identifier subscript letter)
    3743 @item C-c C-a r
    3744 Inserts "\<^raw:>"  (raw LaTeX text).
     3753@item C-c C-a C-r
     3754Inserts "\<^raw:>"  (raw LaTeX text)
     3755@item C-c C-a C-a
     3756Inserts "@@@{text ""@}"  (anti-quotation).
    37453757@end table
    37463758
    37473759Command termination via `@code{;}' is an optional feature of Isar