# HG changeset patch
# User wenzelm
# Date 1465485253 -7200
# Node ID 6d8a67a77bad7b5fc70bea5f845c75d78ce39fca
# Parent  ecaa677d20bc47d5ab0595dc62366385ea397ad2
documentation;

diff -r ecaa677d20bc -r 6d8a67a77bad NEWS
--- a/NEWS	Thu Jun 09 17:13:52 2016 +0200
+++ b/NEWS	Thu Jun 09 17:14:13 2016 +0200
@@ -35,6 +35,10 @@
 * 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').
+
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 
diff -r ecaa677d20bc -r 6d8a67a77bad src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Thu Jun 09 17:13:52 2016 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Thu Jun 09 17:14:13 2016 +0200
@@ -206,6 +206,7 @@
 text \<open>
   \begin{matharray}{rcl}
     @{command_def "bundle"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
+    @{command_def "bundle_definition"} & : & \<open>theory \<rightarrow> local_theory\<close> \\
     @{command_def "print_bundles"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
     @{command_def "include"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
     @{command_def "including"} & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\
@@ -228,6 +229,8 @@
   @{rail \<open>
     @@{command bundle} @{syntax name} '=' @{syntax thms} @{syntax for_fixes}
     ;
+    @@{command bundle_definition} @{syntax name} @'begin'
+    ;
     @@{command print_bundles} ('!'?)
     ;
     (@@{command include} | @@{command including}) (@{syntax name}+)
@@ -241,6 +244,13 @@
   morphisms, when moved into different application contexts; this works
   analogously to any other local theory specification.
 
+  \<^descr> \<^theory_text>\<open>bundle_definition b begin body end\<close> defines a bundle of declarations
+  from the \<open>body\<close> of local theory specifications. It may consist of commands
+  that are technically equivalent to \<^theory_text>\<open>declare\<close> or \<^theory_text>\<open>declaration\<close>, which also
+  includes \<^theory_text>\<open>notation\<close>, for example. Named fact declarations like ``\<^theory_text>\<open>lemmas a
+  [simp] = b\<close>'' or ``\<^theory_text>\<open>lemma a [simp]: B \<proof>\<close>'' are also admitted, but
+  the name bindings are not recorded in the bundle.
+
   \<^descr> \<^theory_text>\<open>print_bundles\<close> prints the named bundles that are available in the
   current context; the ``\<open>!\<close>'' option indicates extra verbosity.