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 9: | Line 9: | ||
* '''Description''': A high-level description of the tactic | * '''Description''': A high-level description of the tactic | ||
* '''Auto-tactic''': ''No'': the tactic cannot be added as auto-tactic. ''Yes'': the tactic can be added as auto-tactic. ''Default'': the tactic is a default auto-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. | |||
Revision as of 21:32, 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.
