Rodin Proof Tactics: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Son No edit summary |
imported>Son No edit summary |
||
| Line 12: | Line 12: | ||
* '''Post-tactic''': ''No'': the tactic cannot be added as a post-tactic. ''Yes'': the tactic can be added as a post-tactic. ''Default'': the tactic is a default post-tactic. | * '''Post-tactic''': ''No'': the tactic cannot be added as a post-tactic. ''Yes'': the tactic can be added as a post-tactic. ''Default'': the tactic is a default post-tactic. | ||
* '''Interactive''': ''No'': the tactic cannot be invoked interactively. ''Global'': The tactic can be invoked from the Proof Control. ''Goal'': The tactic can be invoked from the goal view. ''Hypothesis'': The tactic can be invoked from the hypothesis view. If the tactic can be invoked interactively (i.e. either ''Global'', ''Goal'' or ''Hypothesis''), more information about how this could be done will be given. | |||
Revision as of 21:34, 6 March 2010
This page contains descriptions of the available proof tactics within the RODIN Platform.
For each tactic, the descriptions is as follows:
- ID: The unique ID for each tactic.
- Display: How an application of the tactic is displayed in the proof tree, the auto-tactic preference or the post-tactic preference.
- Description: A high-level description of the tactic
- Auto-tactic: No: the tactic cannot be added as an auto-tactic. Yes: the tactic can be added as an auto-tactic. Default: the tactic is a default auto-tactic.
- Post-tactic: No: the tactic cannot be added as a post-tactic. Yes: the tactic can be added as a post-tactic. Default: the tactic is a default post-tactic.
- Interactive: No: the tactic cannot be invoked interactively. Global: The tactic can be invoked from the Proof Control. Goal: The tactic can be invoked from the goal view. Hypothesis: The tactic can be invoked from the hypothesis view. If the tactic can be invoked interactively (i.e. either Global, Goal or Hypothesis), more information about how this could be done will be given.
