Re: [isabelle] I want to print axiomatization info

I honestly don't think doing such substitutions is of any benefit at all. See if you can make some sense of each definition individually.
Larry Paulson

On 9 Jul 2012, at 20:28, Gottfried Barrow wrote:

> I kind of figured out that in the definitions below, I should start doing some substitutions, like
> P & Q == !R. ((P--> Q-->R) -->  R)
>      == (R = (%x.True)). ((P--> Q-->R) -->  R)
>      == (R = (%x.((%y::bool. y) = (%y. y))). ((P--> Q-->R) -->  R)

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