Differences

This shows you the differences between two versions of the page.

--- pvs:commands [2016/08/29 16:24]
marina [Keyboard Shortcuts]
+++ pvs:commands [2017/09/06 19:33] (current)
jonathan
@@ Line 2: / Line 2: @@
 [[https://wiki.eecs.yorku.ca/project/sel-students/p:tutorials:pvs:shortcuts:start#keyboard_shortcuts|SEL wiki]]
+====== Restarting PVS ======
+If you have a run-away prover command (e.g. GRIND), you can type
+''C-c C-c'' (while in the *pvs* buffer), which will drop you into Lisp.
+At the <rcl> prompt, type (''restore'') to get back to the previous
+sequent.
+If PVS has lost its mind, type ''M-x reset-pvs''. Note. During garbage
+collection, this command will not engage immediately.
+See Survival-Tips.pdf
 ====== Emacs shortcuts with PVS ======
@@ Line 24: / Line 35: @@
 M-x show-proofs-theory   -- Show all proofs of theory
+M-x x-show-current-proof -- show current proof under x11
 step-proof,       prs (C-c C-p s)  Start proof and set up for stepping
@@ Line 249: / Line 261: @@
 </html>
-====== Restarting PVS ======
-If you have a run-away prover command (e.g. GRIND), you can type
-''C-c C-c'' (while in the *pvs* buffer), which will drop you into Lisp.
-At the <rcl> prompt, type (''restore'') to get back to the previous
-sequent.
-If PVS has lost its mind, type ''M-x reset-pvs''. Note. During garbage
-collection, this command will not engage immediately.
-See Survival-Tips.pdf
 ====== Proof Rules ======

Software Engineering Documentation