Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Error in Eisbach syntax diagram

view this post on Zulip Email Gateway (Oct 06 2020 at 21:27):

From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hi!

According to my understanding, the syntax diagram on page 1 of The
Eisbach User Manual says that an alternative in an invocation of the
match method must have exactly one pattern. However, several patterns
are possible, as for instance the first example on page 3 witnesses.
Could the syntax diagram perhaps be fixed? Thanks a lot.

All the best,
Wolfgang

view this post on Zulip Email Gateway (Oct 19 2020 at 00:57):

From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
Hi Wolfgang,

Last updated: Jan 04 2025 at 20:18 UTC