Re: [isabelle] I want to print axiomatization info

On 7/12/2012 1:11 AM, Lars Noschinski wrote:
If you resolve the binder syntax,

!R. (P --> Q --> R) --> R

is the same as

All (%R. (P --> Q -->R) --> R)

where the lambda abstraction has type bool => bool.

Lars, thanks for the tip. Knowing that has saved me some time, and will save me some time.

Thanks again,

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