Re: [isabelle] Implicitly referring to previous facts in the moreover-ultimately paradigm
> I don't see anything unnatural or unnecessary about it. On the
> too much implicit fact management can make Isar proofs hard to read
> hard to maintain, also hard to explain to casual readers who are not
> familiar with the language.
In my opinion, it is indeed a bit strange that the moreover-ultimately
construction chains the implicit facts (so they are available for your
last proof) but you cannot name them.
ultimately have "D" by (blast intro: foo)
which the more experienced Isabelle user might be tempted to write is
not exactly clearer than
using foo[OF ...] .
So we have a construct that provides some nice implicit fact management
for the complicated cases, but not for the simpler cases, where a
simple forward proof does work.
This archive was generated by a fusion of
Pipermail (Mailman edition) and