--- a/NEWS Thu Jun 09 17:14:13 2016 +0200
+++ b/NEWS Fri Jun 10 12:45:34 2016 +0200
@@ -35,9 +35,15 @@
* Old 'header' command is no longer supported (legacy since
Isabelle2015).
-* Command 'bundle_definition' provides a local theory target to define a
-bundle from the body of specification commands (e.g. 'declare',
-'declaration', 'notation', 'lemmas', 'lemma').
+* Command 'bundle' provides a local theory target to define a bundle
+from the body of specification commands (such as 'declare',
+'declaration', 'notation', 'lemmas', 'lemma'). For example:
+
+bundle foo
+begin
+ declare a [simp]
+ declare b [intro]
+end
*** Prover IDE -- Isabelle/Scala/jEdit ***