Difference between revisions of "Extending the Proof Manager"
From Event-B
Jump to navigationJump to searchimported>Son |
imported>Son |
||
| Line 8: | Line 8: | ||
== Adding a New Reasoner == | == Adding a New Reasoner == | ||
| + | |||
| + | A reasoner is added into the Proof Manager using the extension point ''org.eventb.core.seqprover.reasoners''. Below are an example of how to contribute to the extension point. | ||
| + | |||
| + | <extension point="org.eventb.core.seqprover.reasoners"> | ||
| + | <reasoner | ||
| + | class="org.eventb.contributors.seqprover.reasoners.Hyp" | ||
| + | id="hyp" | ||
| + | name="%hypName"/> | ||
| + | </extension> | ||
== Adding a New Tactic == | == Adding a New Tactic == | ||
Revision as of 13:13, 11 September 2008
The Proof Manager is responsible for constructing proofs and maintaining existing proofs associated with proof obligations.
There are two ways for extending the Proof Manager:
- adding a new reasoner.
- adding a new tactic.
Adding a New Reasoner
A reasoner is added into the Proof Manager using the extension point org.eventb.core.seqprover.reasoners. Below are an example of how to contribute to the extension point.
<extension point="org.eventb.core.seqprover.reasoners">
<reasoner
class="org.eventb.contributors.seqprover.reasoners.Hyp"
id="hyp"
name="%hypName"/>
</extension>
