Difference between revisions of "Rodin Proof Tactics"
From Event-B
Jump to navigationJump to searchimported>Son (New page: This page contains descriptions of the available proof tactics within the RODIN Platform.) |
imported>Son |
||
| Line 1: | Line 1: | ||
This page contains descriptions of the available proof tactics within the RODIN Platform. | 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. | ||
| + | |||
| + | * '''Description''': A high-level description of the tactic | ||
| + | |||
| + | * '''Proof tree display''': How an application of the tactic is displayed in the proof tree. | ||
| + | |||
| + | * '''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. | ||
Revision as of 21:30, 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.
- Description: A high-level description of the tactic
- Proof tree display: How an application of the tactic is displayed in the proof tree.
- 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.
