# HG changeset patch
# User wenzelm
# Date 1334494209 -7200
# Node ID e94cc23d434a659b9981a4feac4054d58ed47c5a
# Parent  3f704717a67f1dd068959f5e89873a4b02cbbfe6
some coverage of bundled declarations;

diff -r 3f704717a67f -r e94cc23d434a NEWS
--- a/NEWS	Sun Apr 15 13:21:13 2012 +0200
+++ b/NEWS	Sun Apr 15 14:50:09 2012 +0200
@@ -74,6 +74,14 @@
 Any other local theory specification element works within the "context
 ... begin ... end" block as well.
 
+* Bundled declarations associate attributed fact expressions with a
+given name in the context.  These may be later included in other
+contexts.  This allows to manage context extensions casually, without
+the logical dependencies of locales and locale interpretation.
+
+See commands 'bundle', 'include', 'including' etc. in the isar-ref
+manual.
+
 * Rule composition via attribute "OF" (or ML functions OF/MRS) is more
 tolerant against multiple unifiers, as long as the final result is
 unique.  (As before, rules are composed in canonical right-to-left
diff -r 3f704717a67f -r e94cc23d434a doc-src/IsarRef/Thy/Proof.thy
--- a/doc-src/IsarRef/Thy/Proof.thy	Sun Apr 15 13:21:13 2012 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy	Sun Apr 15 14:50:09 2012 +0200
@@ -294,7 +294,7 @@
 *}
 
 
-subsection {* Facts and forward chaining *}
+subsection {* Facts and forward chaining \label{sec:proof-facts} *}
 
 text {*
   \begin{matharray}{rcl}
@@ -440,7 +440,7 @@
   
     goal: (@{syntax props} + @'and')
     ;
-    longgoal: @{syntax thmdecl}? (@{syntax context_elem} * ) conclusion
+    longgoal: @{syntax thmdecl}? (@{syntax_ref \"includes\"}?) (@{syntax context_elem} * ) conclusion
     ;
     conclusion: @'shows' goal | @'obtains' (@{syntax parname}? case + '|')
     ;
@@ -454,8 +454,8 @@
   \<phi>"} to be put back into the target context.  An additional @{syntax
   context} specification may build up an initial proof context for the
   subsequent claim; this includes local definitions and syntax as
-  well, see the definition of @{syntax context_elem} in
-  \secref{sec:locale}.
+  well, see also @{syntax "includes"} in \secref{sec:bundle} and
+  @{syntax context_elem} in \secref{sec:locale}.
   
   \item @{command "theorem"}~@{text "a: \<phi>"} and @{command
   "corollary"}~@{text "a: \<phi>"} are essentially the same as @{command
diff -r 3f704717a67f -r e94cc23d434a doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Sun Apr 15 13:21:13 2012 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy	Sun Apr 15 14:50:09 2012 +0200
@@ -126,9 +126,10 @@
   "instantiation"}, @{command "overloading"}.
 
   @{rail "
-    @@{command context} (@{syntax nameref} | (@{syntax context_elem}+)) @'begin'
+    @@{command context} @{syntax nameref} @'begin'
     ;
-
+    @@{command context} @{syntax_ref \"includes\"}? (@{syntax context_elem} * ) @'begin'
+    ;
     @{syntax_def target}: '(' @'in' @{syntax nameref} ')'
   "}
 
@@ -140,12 +141,13 @@
   @{keyword "begin"} keyword as well, in order to continue the local
   theory immediately after the initial specification.
 
-  \item @{command "context"}~@{text "elements \<BEGIN>"} opens an
-  unnamed context, by extending the enclosing global or local theory
-  target by the given context elements (@{text "\<FIXES>"}, @{text
-  "\<ASSUMES>"} etc.).  This means any results stemming from
-  definitions and proofs in the extended context will be exported into
-  the enclosing target by lifting over extra parameters and premises.
+  \item @{command "context"}~@{text "bundles elements \<BEGIN>"} opens
+  an unnamed context, by extending the enclosing global or local
+  theory target by the given declaration bundles (\secref{sec:bundle})
+  and context elements (@{text "\<FIXES>"}, @{text "\<ASSUMES>"}
+  etc.).  This means any results stemming from definitions and proofs
+  in the extended context will be exported into the enclosing target
+  by lifting over extra parameters and premises.
   
   \item @{command (local) "end"} concludes the current local theory,
   according to the nesting of contexts.  Note that a global @{command
@@ -187,6 +189,78 @@
   "~~/src/HOL/Isar_Examples/Group_Context.thy"}.  *}
 
 
+section {* Bundled declarations \label{sec:bundle} *}
+
+text {*
+  \begin{matharray}{rcl}
+    @{command_def "bundle"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+    @{command_def "print_bundles"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\
+    @{command_def "include"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
+    @{command_def "including"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
+    @{keyword_def "includes"} & : & syntax \\
+  \end{matharray}
+
+  The outer syntax of fact expressions (\secref{sec:syn-att}) involves
+  theorems and attributes, which are evaluated in the context and
+  applied to it.  Attributes may declare theorems to the context, as
+  in @{text "this_rule [intro] that_rule [elim]"} for example.
+  Configuration options (\secref{sec:config}) are special declaration
+  attributes that operate on the context without a theorem, as in
+  @{text "[[show_types = false]]"} for example.
+
+  Expressions of this form may be defined as \emph{bundled
+  declarations} in the context, and included in other situations later
+  on.  Including declaration bundles augments a local context casually
+  without logical dependencies, which is in contrast to locales and
+  locale interpretation (\secref{sec:locale}).
+
+  @{rail "
+    @@{command bundle} @{syntax target}? \\
+    @{syntax name} '=' @{syntax thmrefs} (@'for' (@{syntax vars} + @'and'))?
+    ;
+    (@@{command include} | @@{command including}) (@{syntax nameref}+)
+    ;
+    @{syntax_def \"includes\"}: @'includes' (@{syntax nameref}+)
+  "}
+
+  \begin{description}
+
+  \item @{command bundle}~@{text "b = decls"} defines a bundle of
+  declarations in the current context.  The RHS is similar to the one
+  of the @{command declare} command.  Bundles defined in local theory
+  targets are subject to transformations via morphisms, when moved
+  into different application contexts; this works analogously to any
+  other local theory specification.
+
+  \item @{command print_bundles} prints the named bundles that are
+  available in the current context.
+
+  \item @{command include}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} includes the declarations
+  from the given bundles into the current proof body context.  This is
+  analogous to @{command "note"} (\secref{sec:proof-facts}) with the
+  expanded bundles.
+
+  \item @{command including} is similar to @{command include}, but
+  works in proof refinement (backward mode).  This is analogous to
+  @{command "using"} (\secref{sec:proof-facts}) with the expanded
+  bundles.
+
+  \item @{keyword "includes"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} is similar to
+  @{command include}, but works in situations where a specification
+  context is constructed, notably for @{command context} and long
+  statements of @{command theorem} etc.
+
+  \end{description}
+
+  Here is an artificial example of bundling various configuration
+  options: *}
+
+bundle trace = [[simp_trace, blast_trace, linarith_trace, metis_trace, smt_trace]]
+
+lemma "x = x"
+  including trace by metis
+
+
 section {* Basic specification elements *}
 
 text {*
diff -r 3f704717a67f -r e94cc23d434a doc-src/IsarRef/Thy/document/Proof.tex
--- a/doc-src/IsarRef/Thy/document/Proof.tex	Sun Apr 15 13:21:13 2012 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex	Sun Apr 15 14:50:09 2012 +0200
@@ -373,7 +373,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Facts and forward chaining%
+\isamarkupsubsection{Facts and forward chaining \label{sec:proof-facts}%
 }
 \isamarkuptrue%
 %
@@ -590,6 +590,10 @@
 \rail@nextbar{1}
 \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
 \rail@endbar
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\indexref{}{syntax}{includes}\hyperlink{syntax.includes}{\mbox{\isa{includes}}}}[]
+\rail@endbar
 \rail@plus
 \rail@nextplus{1}
 \rail@cnont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]
@@ -634,8 +638,8 @@
   \item \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} enters proof mode with
   \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} as main goal, eventually resulting in some fact \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} to be put back into the target context.  An additional \hyperlink{syntax.context}{\mbox{\isa{context}}} specification may build up an initial proof context for the
   subsequent claim; this includes local definitions and syntax as
-  well, see the definition of \hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}} in
-  \secref{sec:locale}.
+  well, see also \hyperlink{syntax.includes}{\mbox{\isa{includes}}} in \secref{sec:bundle} and
+  \hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}} in \secref{sec:locale}.
   
   \item \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} and \hyperlink{command.corollary}{\mbox{\isa{\isacommand{corollary}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} are essentially the same as \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}}, but the facts are internally marked as
   being of a different kind.  This discrimination acts like a formal
diff -r 3f704717a67f -r e94cc23d434a doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Sun Apr 15 13:21:13 2012 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Sun Apr 15 14:50:09 2012 +0200
@@ -187,16 +187,21 @@
   targets, like \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}, \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}, \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}, \hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}.
 
   \begin{railoutput}
-\rail@begin{3}{}
+\rail@begin{1}{}
+\rail@term{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}}[]
+\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
+\rail@term{\isa{\isakeyword{begin}}}[]
+\rail@end
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}}[]
 \rail@bar
-\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
 \rail@nextbar{1}
+\rail@nont{\indexref{}{syntax}{includes}\hyperlink{syntax.includes}{\mbox{\isa{includes}}}}[]
+\rail@endbar
 \rail@plus
-\rail@nont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]
-\rail@nextplus{2}
+\rail@nextplus{1}
+\rail@cnont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]
 \rail@endplus
-\rail@endbar
 \rail@term{\isa{\isakeyword{begin}}}[]
 \rail@end
 \rail@begin{1}{\indexdef{}{syntax}{target}\hypertarget{syntax.target}{\hyperlink{syntax.target}{\mbox{\isa{target}}}}}
@@ -216,11 +221,13 @@
   \hyperlink{keyword.begin}{\mbox{\isa{\isakeyword{begin}}}} keyword as well, in order to continue the local
   theory immediately after the initial specification.
 
-  \item \hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}elements\ {\isaliteral{5C3C424547494E3E}{\isasymBEGIN}}{\isaliteral{22}{\isachardoublequote}}} opens an
-  unnamed context, by extending the enclosing global or local theory
-  target by the given context elements (\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C46495845533E}{\isasymFIXES}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C415353554D45533E}{\isasymASSUMES}}{\isaliteral{22}{\isachardoublequote}}} etc.).  This means any results stemming from
-  definitions and proofs in the extended context will be exported into
-  the enclosing target by lifting over extra parameters and premises.
+  \item \hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}bundles\ elements\ {\isaliteral{5C3C424547494E3E}{\isasymBEGIN}}{\isaliteral{22}{\isachardoublequote}}} opens
+  an unnamed context, by extending the enclosing global or local
+  theory target by the given declaration bundles (\secref{sec:bundle})
+  and context elements (\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C46495845533E}{\isasymFIXES}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C415353554D45533E}{\isasymASSUMES}}{\isaliteral{22}{\isachardoublequote}}}
+  etc.).  This means any results stemming from definitions and proofs
+  in the extended context will be exported into the enclosing target
+  by lifting over extra parameters and premises.
   
   \item \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}} concludes the current local theory,
   according to the nesting of contexts.  Note that a global \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} has a different meaning: it concludes the theory
@@ -259,6 +266,129 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isamarkupsection{Bundled declarations \label{sec:bundle}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+    \indexdef{}{command}{bundle}\hypertarget{command.bundle}{\hyperlink{command.bundle}{\mbox{\isa{\isacommand{bundle}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
+    \indexdef{}{command}{print\_bundles}\hypertarget{command.print-bundles}{\hyperlink{command.print-bundles}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}bundles}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{22}{\isachardoublequote}}} \\
+    \indexdef{}{command}{include}\hypertarget{command.include}{\hyperlink{command.include}{\mbox{\isa{\isacommand{include}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
+    \indexdef{}{command}{including}\hypertarget{command.including}{\hyperlink{command.including}{\mbox{\isa{\isacommand{including}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
+    \indexdef{}{keyword}{includes}\hypertarget{keyword.includes}{\hyperlink{keyword.includes}{\mbox{\isa{\isakeyword{includes}}}}} & : & syntax \\
+  \end{matharray}
+
+  The outer syntax of fact expressions (\secref{sec:syn-att}) involves
+  theorems and attributes, which are evaluated in the context and
+  applied to it.  Attributes may declare theorems to the context, as
+  in \isa{{\isaliteral{22}{\isachardoublequote}}this{\isaliteral{5F}{\isacharunderscore}}rule\ {\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{5D}{\isacharbrackright}}\ that{\isaliteral{5F}{\isacharunderscore}}rule\ {\isaliteral{5B}{\isacharbrackleft}}elim{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} for example.
+  Configuration options (\secref{sec:config}) are special declaration
+  attributes that operate on the context without a theorem, as in
+  \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}show{\isaliteral{5F}{\isacharunderscore}}types\ {\isaliteral{3D}{\isacharequal}}\ false{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} for example.
+
+  Expressions of this form may be defined as \emph{bundled
+  declarations} in the context, and included in other situations later
+  on.  Including declaration bundles augments a local context casually
+  without logical dependencies, which is in contrast to locales and
+  locale interpretation (\secref{sec:locale}).
+
+  \begin{railoutput}
+\rail@begin{6}{}
+\rail@term{\hyperlink{command.bundle}{\mbox{\isa{\isacommand{bundle}}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
+\rail@endbar
+\rail@cr{3}
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
+\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
+\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
+\rail@bar
+\rail@nextbar{4}
+\rail@term{\isa{\isakeyword{for}}}[]
+\rail@plus
+\rail@nont{\hyperlink{syntax.vars}{\mbox{\isa{vars}}}}[]
+\rail@nextplus{5}
+\rail@cterm{\isa{\isakeyword{and}}}[]
+\rail@endplus
+\rail@endbar
+\rail@end
+\rail@begin{2}{}
+\rail@bar
+\rail@term{\hyperlink{command.include}{\mbox{\isa{\isacommand{include}}}}}[]
+\rail@nextbar{1}
+\rail@term{\hyperlink{command.including}{\mbox{\isa{\isacommand{including}}}}}[]
+\rail@endbar
+\rail@plus
+\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
+\rail@nextplus{1}
+\rail@endplus
+\rail@end
+\rail@begin{2}{\indexdef{}{syntax}{includes}\hypertarget{syntax.includes}{\hyperlink{syntax.includes}{\mbox{\isa{includes}}}}}
+\rail@term{\isa{\isakeyword{includes}}}[]
+\rail@plus
+\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
+\rail@nextplus{1}
+\rail@endplus
+\rail@end
+\end{railoutput}
+
+
+  \begin{description}
+
+  \item \hyperlink{command.bundle}{\mbox{\isa{\isacommand{bundle}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}b\ {\isaliteral{3D}{\isacharequal}}\ decls{\isaliteral{22}{\isachardoublequote}}} defines a bundle of
+  declarations in the current context.  The RHS is similar to the one
+  of the \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} command.  Bundles defined in local theory
+  targets are subject to transformations via morphisms, when moved
+  into different application contexts; this works analogously to any
+  other local theory specification.
+
+  \item \hyperlink{command.print-bundles}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}bundles}}}} prints the named bundles that are
+  available in the current context.
+
+  \item \hyperlink{command.include}{\mbox{\isa{\isacommand{include}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} includes the declarations
+  from the given bundles into the current proof body context.  This is
+  analogous to \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}} (\secref{sec:proof-facts}) with the
+  expanded bundles.
+
+  \item \hyperlink{command.including}{\mbox{\isa{\isacommand{including}}}} is similar to \hyperlink{command.include}{\mbox{\isa{\isacommand{include}}}}, but
+  works in proof refinement (backward mode).  This is analogous to
+  \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}} (\secref{sec:proof-facts}) with the expanded
+  bundles.
+
+  \item \hyperlink{keyword.includes}{\mbox{\isa{\isakeyword{includes}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} is similar to
+  \hyperlink{command.include}{\mbox{\isa{\isacommand{include}}}}, but works in situations where a specification
+  context is constructed, notably for \hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}} and long
+  statements of \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}} etc.
+
+  \end{description}
+
+  Here is an artificial example of bundling various configuration
+  options:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{bundle}\isamarkupfalse%
+\ trace\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5F}{\isacharunderscore}}trace{\isaliteral{2C}{\isacharcomma}}\ blast{\isaliteral{5F}{\isacharunderscore}}trace{\isaliteral{2C}{\isacharcomma}}\ linarith{\isaliteral{5F}{\isacharunderscore}}trace{\isaliteral{2C}{\isacharcomma}}\ metis{\isaliteral{5F}{\isacharunderscore}}trace{\isaliteral{2C}{\isacharcomma}}\ smt{\isaliteral{5F}{\isacharunderscore}}trace{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \isacommand{including}\isamarkupfalse%
+\ trace%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ metis%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
 \isamarkupsection{Basic specification elements%
 }
 \isamarkuptrue%