Difference between revisions of "Proof Skeleton View"
imported>Laurent m (→Purpose) |
imported>Laurent |
||
| Line 11: | Line 11: | ||
The Proof Skeleton View is available as other views in the {{menu|Window > Show View > Other > Event-B > Proof Skeleton View}} menu. | The Proof Skeleton View is available as other views in the {{menu|Window > Show View > Other > Event-B > Proof Skeleton View}} menu. | ||
| − | To watch a proof skeleton, simply select a | + | To watch a proof skeleton, simply select a proof obligation or a proof file. |
===View Interpretation=== | ===View Interpretation=== | ||
Revision as of 14:00, 29 January 2009
Purpose
The Proof Skeleton View allows to quickly browse through a proof built either automatically or interactively with the Rodin prover. This view can be used on any proof, independently of the presence of a corresponding proof obligation.
Furthermore, this view allows user to see together proof rules and corresponding sequents.
The Proof Skeleton View
Showing the View
The Proof Skeleton View is available as other views in the menu.
To watch a proof skeleton, simply select a proof obligation or a proof file.
View Interpretation
Proof skeletons are displayed in a two-part view. On the left hand side is the tree structure of rules applied in the proof. On the other side stands the sequent on which the currently selected rule is applied.
The tree can be expanded or collapsed by using [+] and [-] buttons on the upper right corner.
