Extending the Proof Manager: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Son No edit summary |
imported>Son No edit summary |
||
| 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>
