[isabelle-dev] Proposal to use hierarchical heaps with Poly/ML

Lars Hupel hupel at in.tum.de
Thu Nov 12 11:17:46 CET 2015

Hi Japheth,

> A lot of space could be saved if Isabelle saves heaps in this way. For
> our L4.verified project we found a 7× reduction in size.

out of curiousity: How did you arrive at this number? Have you
implemented incremental heaps for Isabelle?


More information about the isabelle-dev mailing list