Controlling backtracking, chaining methods with comma [isa-002F]

Some methods (like erule when there are multiple matching assumptions) are nondeterministic, producing multiple alternative proof states.

The back command interactively explores a different alternative branch produced by the previous step.

lemma "C ∧ D ⟹ A ∧ B ⟹ A" apply (erule conjE) (* could apply to either assumption *) back apply assumption done

This is useful for interactive exploration, but is very brittle and considered poor style.

Instead, we can combine methods with the comma operator ,: The command apply (m1, m2) first runs m1, and then runs m2, accepting only the nondeterministic branches where the second method m2 succeeds. This avoids the need for back:

lemma "C ∧ D ⟹ A ∧ B ⟹ A" apply (erule conjE, assumption) done