assumption solves a subgoal if the consequent is (literally) contained in the set of assumptions.


[The assumption method] 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:

applying assumption now with

apply assumption

solves this goal.


The goal

can not be solved by assumption as 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
reference/assumption.txt · Last modified: 2012/04/13 15:53 by paddy
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki