| changeset 25994 | d35484265f46 |
| parent 25971 | 21953dda56ee |
| child 26006 | c973b4981276 |
--- a/NEWS Sun Jan 27 22:21:35 2008 +0100 +++ b/NEWS Sun Jan 27 22:21:37 2008 +0100 @@ -13,6 +13,11 @@ specified via 3 decimal digits (as in SML). E.g. "foo\095bar" for "foo_bar". +* 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. + *** Pure ***