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

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

A quick look into the sources appears to corroborate your thesis. While
propositions following "shows", "assumes" and "defines" are parsed with
'Parse.propp', the ones following "obtains" are parsed with
'Parse.prop'. The former parses "is", the latter doesn't. Looking
through the history of 'parse_spec.ML' I can't find any evidence of it
being any different in the past.


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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