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.

Cheers
Lars


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



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