Re: [isabelle] Aligning full_prf with proof term



Hi John,

Am 04.10.2011 um 02:49 schrieb John Munroe:

> Anyone got any idea?

From the little I understand about proof terms, they inline all referenced lemmas, which would explain why they can be so huge when you print them at the ML level. The trick would be to write your own traversal function on proof terms that does not enter the lemmas. Hopefully somebody who knows them better can comment further on this.

Regards,

Jasmin






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