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/08/29 15:33] jonathan |
pvs:prover [2017/09/14 16:08] (current) jonathan [Basic] |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== Interaction with Prover ====== | ====== Interaction with Prover ====== | ||
| - | <html> | ||
| - | This is some <span style="color:red;font-size:150%;">inline HTML</span> | ||
| - | </html> | ||
| - | <HTML> | ||
| - | <p style="border:2px dashed red;">And this is some block HTML</p> | ||
| - | </HTML> | ||
| ===== Basic ===== | ===== Basic ===== | ||
| Line 19: | 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 28: | 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.1472484812.txt.gz · Last modified: 2016/08/29 15:33 by jonathan
Page Tools
