[isabelle-dev] NEWS

Makarius makarius at sketis.net
Sun Jan 27 22:23:56 CET 2008

* Theory loader: use_thy (and similar operations) no longer set the
implicit ML context, which was occasionally hard to predict and in
conflict with concurrency.  INCOMPATIBILITY, use ML within Isar which
provides a proper context already.

More information about the isabelle-dev mailing list