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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and