Differences

This shows you the differences between two versions of the page.

--- reference:frule [2011/06/22 12:35] – [Variants] 131.246.161.187
+++ reference:frule [2011/06/22 12:37] (current) – [Relatives] 131.246.161.187
@@ Line 26: / Line 26: @@
 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 ====
@@ Line 45: / Line 45: @@
 ==== Relatives ====
   * ''[[rule]]''
+  * ''[[drule]]''
   * ''[[erule]]''
-  * ''[[frule]]''