Differences

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

--- reference:rule_method [2011/06/22 12:19] – 131.246.161.187
+++ reference:rule_method [2011/06/22 12:27] (current) – [Example] 131.246.161.187
@@ Line 16: / Line 16: @@
 ==== Example ====
+Assume we have a goal
+$\quad[|\ A |] \Longrightarrow A \vee B$
+Applying ''apply (rule disjI1)'' yields the new subgoal
+$\quad [|\ A\ |] \Longrightarrow A$
+which can obviously be solved by one application of ''[[assumption]]''. Note that ''apply (rule(1) disjI)'' is a shortcut for this and immediately solves the goal.
 ==== Non-Example ====