NEWS

--- a/NEWS	Fri Jun 10 17:12:14 2016 +0100
+++ b/NEWS	Fri Jun 10 22:47:25 2016 +0200
@@ -45,6 +45,10 @@
   declare b [intro]
 end
 
+* Command 'unbundle' is like 'include', but works within a local theory
+context. Unlike "context includes ... begin", the effect of 'unbundle'
+on the target context persists, until different declarations are given.
+
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***