Re: [isabelle] Printing instantiations

There has been much work on reducing the size of proof terms by the proof carrying code community.

Quoting Lawrence Paulson <lp15 at>:

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.

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

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