src/Doc/Isar_Ref/Spec.thy

   \end{description}
 
   Here is an artificial example of bundling various configuration
   options:\<close>
 
+(*<*)experiment begin(*>*)
 bundle trace = [[simp_trace, linarith_trace, metis_trace, smt_trace]]
 
 lemma "x = x"
   including trace by metis
+(*<*)end(*>*)
 
 
 section \<open>Term definitions \label{sec:term-definitions}\<close>
 
 text \<open>

   other serves as parameter.  Here are examples for these two cases:
 
   \end{description}
 \<close>
 
+(*<*)experiment begin(*>*)
   attribute_setup my_rule =
     \<open>Attrib.thms >> (fn ths =>
       Thm.rule_attribute
         (fn context: Context.generic => fn th: thm =>
           let val th' = th OF ths

     \<open>Attrib.thms >> (fn ths =>
       Thm.declaration_attribute
         (fn th: thm => fn context: Context.generic =>
           let val context' = context
           in context' end))\<close>
+(*<*)end(*>*)
 
 text \<open>
   \begin{description}
 
   \item @{attribute ML_print_depth} controls the printing depth of the ML