====== Interaction with Prover ======


===== Basic =====

  * From the command line: ''pvs''
  * Change context: C-c C-c
  * Create new PVS file: M-x nf
  * Type Check: M-x tcp
  * Show type correctness conjectures: M-x tccs
  * pretty print expanded: C-c C-p e
  * Prove a Conjecture:
  * Prove the whole file: C-c C-p f
  * View prelude file: M-x vpf
  * View proof status: ''M-x spf''
  * Display the proof in progress: ''M-x show-current-proof  ''        

ProofLite scripts can be created from proofs in two ways:
(1) Place the cursor on the formula for which you want to create
a ProofLite script and issue the Emacs command: M-x insert-prooflite-script (C-c 2p). T
he ProofLite script is automatically inserted after the formula.
(2) Issue the command: M-x display-prooflite-script (C-c dp)
and enter the name of a formula. The ProofLite script of that
formula is displayed in the buffer "ProofLite".

===== Commands =====
  * Introduce all types in formula: ''(all-typepreds)''
  * ''(typepred a b c)''