[isabelle] Syntax diagram for obtains allows "is" bindings

Dear Isar experts,

The syntax diagrams in the isar-ref manual (section 6.2.4) for obtains allow is-bindings for the propositions in where clauses - at least that is how I understand them. Unfortunately, I get syntax errors at "(" when I try to use them as in

lemma obtains y ys where "x = y # ys" (is "?foo y ys")

Apparently, the documentation and the system do not agree in this case. Also, the syntax diagram for "case" misses the possibility of not binding variables and omitting the where part.


PS: Two unanswered posts are related:

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