[isabelle] Implicitly referring to previous facts in the moreover-ultimately paradigm
Dear Isabelle users,
In the from-have paradigm, we can implicitly refer to the previous proved fact(s) using the “this” keyword. I was wondering if we can similarly refer to collected results implicitly in the moreover-ultimately paradigm? If not, would that be a good feature for future Isabelle?
Here is a minimal example:
fix A B D::bool
assume foo:"A ⟹ B ⟹ D"
have "A" "B" sorry
from foo[OF this(1) this(2)] (*here, we can implicitly refer to the previous facts
using the "this" keyword*)
have "D" .
have "A" sorry
moreover have "B" sorry
ultimately have "D"
using foo[OF (*I wish to implicitly refer to A and B here,
like using the "this" keyword previously*)]
This archive was generated by a fusion of
Pipermail (Mailman edition) and