User Tools
reference:frule
Differences
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] (current) 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]]'' | ||
reference/frule.1308738955.txt.gz · Last modified: 2011/06/22 12:35 by 131.246.161.187
Page Tools
