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?




PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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