Emacs Cheat Sheet
=================

C-x  means  "Control-x"  (deutsch: Steuerung-x Strg-x)
M-x  means  "Alt-x"

File commands

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

Undo and abort

C-_      undo
C-g      "quit"

Cut&paste commands

C-space  begin selection
C-k      kill line
C-y      "yank" (paste)
M-y      cycle kill-ring
C-w      cut
M-w      copy  ("Alt-w")

Window commands

C-x 2    split window
C-x 0    delete window
C-x 1    keep only this window
C-x 3    split horizontally

Frame commands 
(like window commands, but prefix C-x 5 instead of C-x)

C-x 5 2  ... frame
C-x 5 0  

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

M-x new-theory

(Example:)

A,B,C,D : boolean

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

Proving proposition under cursor:
M-x typecheck  ==  C-c t
M-x prove      ==  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")		 
(expand* "def1" "def2")	 
			 
M-x change-context        ;; change directory