Re: [isabelle] Printing instantiations



Hi Steve,

> Thanks. I have another question which may require working at the ML
> level: If some lemma can be proved at the Isar level, are there ways to
> extract out the instantiations of each term in the lemma? Does the proof
> of the lemma need to be at the ML level as well?

I am a little bit lost since I don't understand what you want.  A lemma
proposition "as it is" is just a term on its own.  So what do you mean
exactly by "instantiation of each term in the lemma"?  Have you got an
example Isar snippet?

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.