Extending the Proof Manager: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Son New page: The Proof Manager is to ... |
imported>Son No edit summary |
||
Line 1: | Line 1: | ||
The [[Proof Manager]] is | 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 [[Reasoners|reasoner]]. | |||
# adding a new [[Tactics|tactic]]. | |||
== Adding a New Reasoner == | |||
== Adding a New Tactic == |
Revision as of 13:06, 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.