Re: [isabelle] Aligning full_prf with proof term
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and