# 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 \ \begin{matharray}{rcl} @{command_def "bundle"} & : & \local_theory \ local_theory\ \\ + @{command_def "bundle_definition"} & : & \theory \ local_theory\ \\ @{command_def "print_bundles"}\\<^sup>*\ & : & \context \\ \\ @{command_def "include"} & : & \proof(state) \ proof(state)\ \\ @{command_def "including"} & : & \proof(prove) \ proof(prove)\ \\ @@ -228,6 +229,8 @@ @{rail \ @@{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>\bundle_definition b begin body end\ defines a bundle of declarations + from the \body\ of local theory specifications. It may consist of commands + that are technically equivalent to \<^theory_text>\declare\ or \<^theory_text>\declaration\, which also + includes \<^theory_text>\notation\, for example. Named fact declarations like ``\<^theory_text>\lemmas a + [simp] = b\'' or ``\<^theory_text>\lemma a [simp]: B \\'' are also admitted, but + the name bindings are not recorded in the bundle. + \<^descr> \<^theory_text>\print_bundles\ prints the named bundles that are available in the current context; the ``\!\'' option indicates extra verbosity.