src/Doc/Isar_Ref/Generic.thy

   name.  This form of context declaration works particularly well with
   commands such as @{command "declare"} or @{command "using"} like
   this:
 \<close>
 
+(*<*)experiment begin(*>*)
 declare [[show_main_goal = false]]
 
 notepad
 begin
   note [[show_main_goal = true]]
 end
+(*<*)end(*>*)
 
 text \<open>For historical reasons, some tools cannot take the full proof
   context into account and merely refer to the background theory.
   This is accommodated by configuration options being declared as
   ``global'', which may not be changed within a local context.

 
   Ordered rewriting with the combination of A, C, and LC sorts a term
   lexicographically --- the rewriting engine imitates bubble-sort.
 \<close>
 
-locale AC_example =
+experiment
   fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infix "\<bullet>" 60)
   assumes assoc: "(x \<bullet> y) \<bullet> z = x \<bullet> (y \<bullet> z)"
   assumes commute: "x \<bullet> y = y \<bullet> x"
 begin
 

   rewrite step. For example:
 
   \end{description}
 \<close>
 
+(*<*)experiment begin(*>*)
 declare conjI [simp_break]
 declare [[simp_break "?x \<and> ?y"]]
+(*<*)end(*>*)
 
 
 subsection \<open>Simplification procedures \label{sec:simproc}\<close>
 
 text \<open>Simplification procedures are ML functions that produce proven

   control over rule application, beyond higher-order pattern matching.
   Declaring @{thm unit_eq} as @{attribute simp} directly would make
   the Simplifier loop!  Note that a version of this simplification
   procedure is already active in Isabelle/HOL.\<close>
 
+(*<*)experiment begin(*>*)
 simproc_setup unit ("x::unit") =
   \<open>fn _ => fn _ => fn ct =>
     if HOLogic.is_unit (Thm.term_of ct) then NONE
     else SOME (mk_meta_eq @{thm unit_eq})\<close>
+(*<*)end(*>*)
 
 text \<open>Since the Simplifier applies simplification procedures
   frequently, it is important to make the failure check in ML
   reasonably fast.\<close>
 

   \end{description}
 
   As an example, consider the following alternative subgoaler:
 \<close>
 
-ML \<open>
+ML_val \<open>
   fun subgoaler_tac ctxt =
     assume_tac ctxt ORELSE'
     resolve_tac ctxt (Simplifier.prems_of ctxt) ORELSE'
     asm_simp_tac ctxt
 \<close>

   All members of a wrapper list are applied in turn to the respective
   step tactic.
 
   Initially the two wrapper lists are empty, which means no
   modification of the step tactics. Safe and unsafe wrappers are added
-  to a claset with the functions given below, supplying them with
+  to the context with the functions given below, supplying them with
   wrapper names.  These names may be used to selectively delete
   wrappers.
 
   \begin{description}