NEWS
changeset 37868 59eed00bfd8e
parent 37820 ffaca9167c16
child 37939 965537d86fcc
--- a/NEWS	Wed Jul 21 14:27:05 2010 +0200
+++ b/NEWS	Wed Jul 21 15:02:51 2010 +0200
@@ -103,6 +103,15 @@
   similar to inductive_cases.
 
 
+*** ML ***
+
+* ML antiquotations @{theory} and @{theory_ref} refer to named
+theories from the ancestry of the current context, not any accidental
+theory loader state as before.  Potential INCOMPATIBILITY, subtle
+change in semantics.
+
+
+
 New in Isabelle2009-2 (June 2010)
 ---------------------------------