User Tools
pvs:prover
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
pvs:prover [2016/09/04 17:52] jonathan |
pvs:prover [2017/09/14 16:08] (current) jonathan [Basic] |
||
|---|---|---|---|
| Line 13: | Line 13: | ||
| * Prove the whole file: C-c C-p f | * Prove the whole file: C-c C-p f | ||
| * View prelude file: M-x vpf | * 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: | ProofLite scripts can be created from proofs in two ways: | ||
| Line 22: | Line 24: | ||
| formula is displayed in the bu ffer "ProofLite". | formula is displayed in the bu ffer "ProofLite". | ||
| + | ===== Commands ===== | ||
| + | * Introduce all types in formula: ''(all-typepreds)'' | ||
| + | * ''(typepred a b c)'' | ||
pvs/prover.1473011576.txt.gz · Last modified: 2016/09/04 17:52 by jonathan
Page Tools
