Re: [isabelle] structure of a theorem

Hi Mamoun,

>    in Isar, given a theorem, is there a way to access to the terms of
> its assumptions and
> conclusion?

short answer: no there isn't such.

Maybe, I guess, you have some proofs and want to find ways to organize
them in a nice fashion -- there are a couple of such organization
principles possible in Isar, but from your toy example it is impossible
to glimpse what could be helpful for you.  So, if you like, just post
more context on here and maybe we can find a device for the problem you
actually want to solve.




PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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