Re: [isabelle] Printing instantiations

Nothing ever changes. The prohibitive size of proof terms is the reason Robin Milner invented the LCF approach in the first place. The machine he was using had about 1 MB of memory.

On 17 Jun 2010, at 11:23, Makarius wrote:

> For the coming Isabelle2009-2 we had to give up that convenience, because HOL proofs have grown too fat, so there will be the separate HOL-Proofs image that has to be build manually.

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