| changeset 39557 | fe5722fce758 |
| parent 39513 | fce2202892c4 |
| child 39616 | 8052101883c3 |
--- a/NEWS Mon Sep 20 15:29:53 2010 +0200 +++ b/NEWS Mon Sep 20 16:05:25 2010 +0200 @@ -244,6 +244,10 @@ *** ML *** +* 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. + * Discontinued Output.debug. Minor INCOMPATIBILITY, use plain writeln instead (or tracing for high-volume output).