This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
reference:frule [2011/06/22 12:35] 131.246.161.187 [Variants] |
reference:frule [2011/06/22 12:37] 131.246.161.187 [Relatives] |
||
---|---|---|---|
Line 26: | Line 26: | ||
Applying ''apply (drule mp)'' yields new goals | Applying ''apply (drule mp)'' yields new goals | ||
- | $\quad A \Longrightarrow A$ | + | $\quad [|\ A \longrightarrow B; A\ |] \Longrightarrow A$ |
- | $\quad[|\ A; B\ |] \Longrightarrow B$ | + | $\quad[|\ A \longrightarrow B; A; B\ |] \Longrightarrow B$ |
- | which can both be solved by ''[[assumption]]''. Note that ''apply (drule(2) mp)'' is a shortcut for this and immediately solves the goal. | + | which can both be solved by ''[[assumption]]''. Note that ''apply (frule(2) mp)'' is a shortcut for this and immediately solves the goal. |
==== Non-Example ==== | ==== Non-Example ==== | ||
Line 45: | Line 45: | ||
==== Relatives ==== | ==== Relatives ==== | ||
* ''[[rule]]'' | * ''[[rule]]'' | ||
+ | * ''[[drule]]'' | ||
* ''[[erule]]'' | * ''[[erule]]'' | ||
- | * ''[[frule]]'' |