PVS Cheat Sheet
===============

C-x C-f find-file
C-x C-s save

M-x new-theory

(Example:)

A,B,C,D : VAR boolean

notAnd : PROPOSITION
        NOT (A AND B) IFF NOT A OR NOT B

M-x prove  ;; C-c p ,  [C-c C-p] , C-c C-p C-p

(skolem!)            ;; auto-introduce names
(skolem 1 ("A" "B")) ;; provide names
(skolem 1 (A B))     ;; introduces "a" "b"
(flatten)            ;; apply one-premise sequent rules
(split)              ;; apply two-premise sequent rules

(M-x x-show-proof)         ;; brings-up funny window
(M-x x-show-current-proof) ;; when proof is not completed
(M-x latex-proof-view)     ;; full proof

(quit) ;; abort proof
(fail) ;; retract proof

(prop)  ;; propositional simplification
(grind) ;; holzhammer

(expand "def")

M-x change-context