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>