[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.

Best,
Andreas

PS: Two unanswered posts are related:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2011-November/msg00002.html
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-June/msg00050.html




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