[isabelle] Error in Eisbach syntax diagram


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,

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