Difference between revisions of "Extension Proof Rules"
From Event-B
Jump to navigationJump to searchimported>Nicolas (added rules SIMP_SPECIAL_COND_BTRUE and SIMP_SPECIAL_COND_BFALSE) |
imported>Nicolas m (Extension Rewrite Rules moved to Extension Proof Rules: Gathering rewrite and inference rules for extensions in the same page.) |
(No difference)
| |
Revision as of 10:23, 9 September 2010
Rules that are marked with a * in the first column are implemented in the latest version of Rodin. Rules without a * are planned to be implemented in future versions. Other conventions used in these tables are described in The_Proving_Perspective_(Rodin_User_Manual)#Rewrite_Rules.
| Name | Rule | Side Condition | A/M | |
|---|---|---|---|---|
SIMP_SPECIAL_COND_BTRUE |
 |
A | ||
SIMP_SPECIAL_COND_BFALSE |
 |
A |
