assumption solves a subgoal if the consequent is (literally) contained in the set of assumptions.
assumptionmethod] proves a subgoal by finding a matching assumption.
(From “Isabelle/HOL – A Proof Assisstant for Higher-Order Logic”, Nipkow et al, 2009)
Assume you have this goal in your proof state:
assumption now with
solves this goal.
can not be solved by
a is not included in the set of assumptions. You have to eliminate the first.
assumption+ applies as many assumption steps in sequence as possible