| changeset 39616 | 8052101883c3 |
| parent 39557 | fe5722fce758 |
| child 39644 | ad436fa9fc5b |
--- a/NEWS Wed Sep 22 17:46:59 2010 +0200 +++ b/NEWS Wed Sep 22 18:21:48 2010 +0200 @@ -244,6 +244,9 @@ *** ML *** +* Renamed setmp_noncritical to Unsynchronized.setmp to emphasize its +meaning. + * Renamed structure PureThy to Pure_Thy and moved most of its operations to structure Global_Theory, to emphasize that this is rarely-used global-only stuff.