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:

BTW: Searching for PROP in the reference manual, I learned a new trick: If you want e.g. to apply a rule X: "A ==> B ==> C", but only have the "B" available as a fact, you can do

   from _ and `B` have "C" apply (rule X)

to skip the first precondition of X and don't need to resort to things like

  have "C"
    apply (rule X)
    prefer 2
    apply (fact `B`)

or

  have "C" apply (rule X[OF _ `B`])

Judging from the few occurrences in Isabelle and the AFP, I guess this technique is not very well known.

  -- Lars




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