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

On Wed, 17 Jul 2013, Lars Noschinski wrote:

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:

See isar-ref manual section "7.4 The Pure Syntax". This should be mostly up-to-date, but it is a long way to go through the manual to find the way to PROP. (It is rarely needed in regular practice.)


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