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.

Cheers,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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