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