Re: [isabelle] Can't abbreviate ==> like I want; something to do with prop

On 17.07.2013 07:24, Lars Noschinski wrote:
You can instruct Isabelle to not insert Trueprop automatically by
prefixing it with the PROP syntax:

Actually, is the PROP syntax documented somewhere? I looked in the index of the reference manual and the best I could find was the the following comment in the reference manual in the chapter about inner syntax:

| aprop denotes atomic propositions, which are embedded into regular
| prop by means of an explicit PROP token.
| Terms of type prop with non-constant head, e.g. a plain variable, are
| printed in this form. Constants that yield type prop are expected to
| provide their own concrete syntax; otherwise the printed version will
| appear like logic and cannot be parsed again as prop.

  -- Lars

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