# Picking this and calculation in Isabelle/JEdit output

This is a follow-up to

How to write a low-level proof in Isar?

Having

lemma por_qandr_imp_porq: assumes "p ∨ (q ∧ r)" shows "p ∨ q"
proof -
note assms
moreover
have "p ⟹ p ∨ q"
by (rule p_imp_porq)
moreover
have "q ∧ r ⟹ p ∨ q"
by (rule qandr_imp_porq)
ultimately
show ?thesis
by (rule disjE[of p "q∧r" "p∨q"])
qed


if I point the cursor after ultimately, Isabelle/JEdit's Output window shows

proof (chain)
picking this:
p ∨ q ∧ r
p ⟹ p ∨ q
q ∧ r ⟹ p ∨ q
calculation:
p ∨ q ∧ r
p ⟹ p ∨ q
q ∧ r ⟹ p ∨ q


where calculation is in grey background. The contents of the picking this and the calculation parts are identical, but what is the difference between the two in their meaning?

At each step accumulating facts (i.e., each of moreover and the final ultimately), the proof state will show the fact calculation—which you can quote inside the proof, by the way.
AFAIK, this is redundant in the final step since both lists are the same. But the picking this message is useful since it indicates that those facts will be used (“chained”) for the next inference (which does not occur at moreover steps). If you actually want to use all of them amidst that block, you may invoke moreover from calculation.