Re: [isabelle] calculational reasoning for transitive relations



Tried now and it works, including with all combinations: 
transtitivity of <o versus <=o, of <=o versus <o, of <=o versus =o, etc.

Thank you, that was easy.  :)

This database-driven customization style for Isabelle does marvels, I should 
become 

more familiar with it.  

Best regards, 
   Andrei 



----- Original Message ----
From: Brian Huffman <brianh at cs.pdx.edu>
To: Andrei Popescu <uuomul at yahoo.com>
Cc: cl-isabelle-users at lists.cam.ac.uk; Joachim Breitner 
<mail at joachim-breitner.de>
Sent: Wed, September 22, 2010 8:35:59 PM
Subject: 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
> possible.

I think all you need to do is declare the transitivity rules with the
[trans] attribute. Have either of you tried this?

- Brian










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