Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] [RC3]: Word omission in isar-ref

view this post on Zulip Email Gateway (Aug 19 2022 at 15:22):

From: René Neumann <rene.neumann@in.tum.de>
Hi,

I noticed the following omission in isar-ref §6.2.4, last paragraph:

The optional case names of obtains have a twofold meaning: (1) during
the [something is missing here] of this claim they [..]

Probably 'proof' is missing there.

view this post on Zulip Email Gateway (Aug 19 2022 at 15:24):

From: Makarius <makarius@sketis.net>
Yes, and there are more oddities in the wording. I am tuning this for the
next release candidate.

Makarius

Last updated: Apr 30 2024 at 04:19 UTC