[isabelle-dev] Data slots for runtime compiler invocation
Makarius
makarius at sketis.net
Mon Jan 10 18:15:37 CET 2011
On Mon, 10 Jan 2011, Florian Haftmann wrote:
> Recently I changed the interface for invoking the compiler at runtime on
> generated code to use proof data slots rather than unsychronized
> references. The consequence is that there are a lot of non-joinable
> proof data slots laying around in the same module, cf.
> http://isabelle.in.tum.de/reports/Isabelle/rev/f6ab14e61604
Which are the non-joinable ones in particular? Did I overlook anything
important?
Makarius
More information about the isabelle-dev
mailing list