Corey Lewis

> The `capDL-tool` will need some changes in `PrintIsabelle.hs` so that it produces output that is consistent with the verification `capDL` specification. In particular, the verification specification doesn't know about...

> Hmm, I guess that an easier alternative would be to update the verification specification's TCB slots instead. I don't think that that would affect any of the proofs and...

I have to admit that I don't remember the details for this anymore or what the use case for it was, but it does look like you're right and that...

Good catch, it should be pretty straightforward to escape those quotes. However, looking at this has made me consider whether arguments like the `FrameFill` should be printed at all in...