[isabelle-dev] Speed of @{thm}

Makarius makarius at sketis.net
Sun Aug 12 20:41:42 CEST 2012

On Sun, 12 Aug 2012, Jasmin Blanchette wrote:

>> Reading this again, I don't understand it.  Which detail made the 
>> difference?
> Creating a "my_ctxt" function that indirectly called 
> "ML_Context.the_local_context". But I haven't tried this in Isabelle, 
> only in my mock-up theory.

Never mind.  I have yet another refinement in the pipeline, so in a minute 
the problem might actually be solved.


More information about the isabelle-dev mailing list