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? Cheers Lars