Re: [isabelle] Unable to prove easy existential "directly"
On Fri, 19 Jul 2013, Tobias Nipkow wrote:
Don't worry, it is alive and kicking.
According to canonical jargon on this mailing list, "old fashioned" means
it is not even "legacy" yet. It just means old-fashioned.
Nonetheless, there is no reason to encumber new learners of Isar with old
habits drawn from Mizar. The latter cannot even use "then obtain ..." or
"obtain ... then". I also want to do Mizar justice in avoiding confusion
of its "hence" and "thus" that have a quite different meaning there.
This archive was generated by a fusion of
Pipermail (Mailman edition) and