--- a/NEWS Wed Apr 28 12:18:49 2010 +0200
+++ b/NEWS Wed Apr 28 12:21:55 2010 +0200
@@ -116,6 +116,9 @@
context -- without introducing dependencies on parameters or
assumptions, which is not possible in Isabelle/Pure.
+* Command 'defaultsort' is renamed to 'default_sort', it works within
+a local theory context. Minor INCOMPATIBILITY.
+
* Proof terms: Type substitutions on proof constants now use canonical
order of type variables. INCOMPATIBILITY: Tools working with proof
terms may need to be adapted.