User Tools

Site Tools


reference:rule_method

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
reference:rule_method [2011/06/22 12:19]
131.246.161.187
reference:rule_method [2011/06/22 12:27] (current)
131.246.161.187 [Example]
Line 16: Line 16:
  
 ==== Example ==== ==== 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 ==== ==== Non-Example ====
reference/rule_method.txt ยท Last modified: 2011/06/22 12:27 by 131.246.161.187