Re: [isabelle] Printing instantiations



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

Randy
--
Quoting Lawrence Paulson <lp15 at cam.ac.uk>:

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.
Larry

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.