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.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.