User Tools
reference:frule
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Last revision Both sides next revision | ||
|
reference:frule [2011/06/22 12:35] 131.246.161.187 [Variants] |
reference:frule [2011/06/22 12:36] 131.246.161.187 [Example] |
||
|---|---|---|---|
| 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 ==== | ||
reference/frule.txt ยท Last modified: 2011/06/22 12:37 by 131.246.161.187
Page Tools
