diff -r 454dfdaf021d -r 2d9918f5b33c NEWS
--- a/NEWS	Fri Feb 23 13:09:45 2018 +0100
+++ b/NEWS	Fri Feb 23 14:12:48 2018 +0100
@@ -167,6 +167,15 @@
 latex and bibtex process. Minor INCOMPATIBILITY.
 
 
+*** Isar ***
+
+* Command 'interpret' no longer exposes resulting theorems as literal
+facts, notably for the \<open>prop\<close> notation or the "fact" proof method. This
+improves modularity of proofs and scalability of locale interpretation.
+Rare INCOMPATIBILITY, need to refer to explicitly named facts instead
+(e.g. use 'find_theorems' or 'try' to figure this out).
+
+
 *** HOL ***
 
 * Clarifed theorem names: