Table of Contents

`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