Difference between revisions of "Extending the Proof Manager"
From Event-B
Jump to navigationJump to searchimported>Son (New page: The Proof Manager is to ...) |
imported>Son |
||
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.