Re: [isabelle] calculational reasoning for transitive relations
On Wed, Sep 22, 2010 at 1:20 PM, Andrei Popescu <uuomul at yahoo.com> wrote:
> Joachim Breitner wrote:
>>> Also, it would be nice if the transitivity rules for <o, <=o, =o were
>>> set up to work with Isar’s "also... also... finally".
> Good point. I actually though about this too, but did not investigate if it is
I think all you need to do is declare the transitivity rules with the
[trans] attribute. Have either of you tried this?
This archive was generated by a fusion of
Pipermail (Mailman edition) and