pvs:prover

This is an old revision of the document!

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

pvs/prover.1471974712.txt.gz · Last modified: 2016/08/23 17:51 by jonathan