Proof Skeleton View - Revision history

imported>Ladenberger at 12:50, 27 September 2011

2011-09-27T12:50:43Z

← Older revision		Revision as of 12:50, 27 September 2011
Line 1:		Line 1:
	~~{\| class="wikitable" style="font-style:italic; text-align: center; font-size:120%; border: 3px dashed red;"~~
	\|-
	~~! scope="col" \| Do not edit! This content has been migrated to Subversion.~~
	\|-
	~~\|([http://handbook.event-b.org Nightly Handbook Build])~~
	\|}

	==Purpose==		==Purpose==

2011-09-19T14:14:24Z

← Older revision		Revision as of 14:14, 19 September 2011
Line 1:		Line 1:
			{\| class="wikitable" style="font-style:italic; text-align: center; font-size:120%; border: 3px dashed red;"
			\|-
			! scope="col" \| Do not edit! This content has been migrated to Subversion.
			\|-
			\|([http://handbook.event-b.org Nightly Handbook Build])
			\|}

	==Purpose==		==Purpose==

2010-01-12T16:04:35Z

Copy/Paste to Proof Tree

← Older revision		Revision as of 16:04, 12 January 2010
Line 31:		Line 31:

	{\| cellspacing="15"		{\| cellspacing="15"
	\|[[Image:proofSkeleton_copyPaste_Copy.png]]		\|[[Image:proofSkeleton_copyPaste_Copy.png\|400px]]
	\|[[Image:proofSkeleton_copyPaste_Paste.png]]		\|[[Image:proofSkeleton_copyPaste_Paste.png\|400px]]
	\|[[Image:proofSkeleton_copyPaste_End.png]]		\|[[Image:proofSkeleton_copyPaste_End.png\|400px]]
	\|}		\|}

	[[Category:User documentation]]		[[Category:User documentation]]
	[[Category:Proof]]		[[Category:Proof]]

2010-01-12T16:01:30Z

Copy/Paste to Proof Tree

← Older revision		Revision as of 16:01, 12 January 2010
Line 25:		Line 25:
	The copy/paste feature allows to reuse a stored proof into a new proof. Starting from the following configuration:		The copy/paste feature allows to reuse a stored proof into a new proof. Starting from the following configuration:

	[[Image:proofSkeleton_copyPaste_Start.~~jpg~~]]		[[Image:proofSkeleton_copyPaste_Start.png\|800px]]

	where the proof we are working on (top left) is similar to another proof whose skeleton is displayed on bottom left.		where the proof we are working on (top left) is similar to another proof whose skeleton is displayed on bottom left.
Line 31:		Line 31:

	{\| cellspacing="15"		{\| cellspacing="15"
	\|[[Image:proofSkeleton_copyPaste_Copy.~~jpg~~]]		\|[[Image:proofSkeleton_copyPaste_Copy.png]]
	\|[[Image:proofSkeleton_copyPaste_Paste.~~jpg~~]]		\|[[Image:proofSkeleton_copyPaste_Paste.png]]
	\|[[Image:proofSkeleton_copyPaste_End.~~jpg~~]]		\|[[Image:proofSkeleton_copyPaste_End.png]]
	\|}		\|}

	[[Category:User documentation]]		[[Category:User documentation]]
	[[Category:Proof]]		[[Category:Proof]]

2010-01-12T15:53:01Z

The Proof Skeleton View

@@ Line 21: / Line 21: @@
 The tree can be expanded or collapsed by using [+] and [-] buttons on the upper right corner.
 [[Category:User documentation]]
 [[Category:Proof]]

2009-10-14T12:26:13Z

← Older revision		Revision as of 12:26, 14 October 2009
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 proof obligation or a proof file.		To watch a proof skeleton, simply select a proof obligation or a proof file in the Event-B Explorer.

	===View Interpretation===		===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.		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 right-hand side stands the sequent on which the currently selected rule is applied. The proof which is displayed is the one stored in the proof file on disk, never the one which is currently edited through the proof control. This can be very handy as it can allow one to see the previous proof of a proof obligation while working on a new proof of it.

	[[Image:proofSkeletonView.jpg]]		[[Image:proofSkeletonView.jpg]]

2009-08-12T12:54:58Z

← Older revision		Revision as of 12:54, 12 August 2009
Line 23:		Line 23:

	[[Category:User documentation]]		[[Category:User documentation]]
			[[Category:Proof]]

2009-04-06T14:05:27Z

← Older revision		Revision as of 14:05, 6 April 2009
Line 22:		Line 22:


	[[Category:User ~~Documentation~~]]		[[Category:User documentation]]

2009-01-29T14:00:44Z

Showing the View

← Older revision		Revision as of 14:00, 29 January 2009
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 ~~proved predicate in the~~ obligation ~~explorer,~~ or a proof file ~~in the editor~~.		To watch a proof skeleton, simply select a proof obligation or a proof file.

	===View Interpretation===		===View Interpretation===

2009-01-29T13:58:46Z

Purpose

← Older revision		Revision as of 13:58, 29 January 2009
Line 1:		Line 1:
	==Purpose==		==Purpose==

	The Proof Skeleton View allows to quickly browse through a proof ~~build~~ 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.		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.		Furthermore, this view allows user to see together proof rules and corresponding sequents.