doc-src/Ref/simplifier.tex

 \begin{ttbox}
 simpset        : unit -> simpset
 simpset_ref    : unit -> simpset ref
 simpset_of     : theory -> simpset
 simpset_ref_of : theory -> simpset ref
+SIMPSET        : (simpset -> tactic) -> tactic
+SIMPSET'       : (simpset -> 'a -> tactic) -> 'a -> tactic
 print_simpset  : theory -> unit
 \end{ttbox}
 
 Each theory contains a current simpset\index{simpset!current} stored
 within a private ML reference variable.  This can be retrieved and

   from theory $thy$.
   
 \item[\ttindexbold{simpset_ref_of} $thy$;] retrieves the simpset
   reference variable from theory $thy$.
 
+\item[\ttindexbold{SIMPSET} $tacf$, \ttindexbold{SIMPSET'} $tacf'$]
+  are tacticals that make a tactic depend on the implicit current
+  simpset of the theory associated with the proof state they are
+  applied on.
+
 \item[\ttindexbold{print_simpset} $thy$;] prints the current simpset
   of theory $thy$ in the same way as \texttt{print_ss}.
 
 \end{ttdescription}
+
+\begin{warn}
+  There is a subtle difference between \texttt{(SIMPSET'~$tacf$)} and
+  \texttt{($tacf$~(simpset()))}.  For example \texttt{(SIMPSET'
+    simp_tac)} would depend on the theory of the proof state it is
+  applied to, while \texttt{(simp_tac (simpset()))} implicitly refers
+  to the current theory context.  Both are usually the same in proof
+  scripts, provided that goals are only stated within the current
+  theory.  Robust programs would not count on that, of course.
+\end{warn}
 
 
 \subsection{Rewrite rules}
 \begin{ttbox}
 addsimps : simpset * thm list -> simpset \hfill{\bf infix 4}

 simp_tac               : simpset -> int -> tactic
 asm_simp_tac           : simpset -> int -> tactic
 full_simp_tac          : simpset -> int -> tactic
 asm_full_simp_tac      : simpset -> int -> tactic
 safe_asm_full_simp_tac : simpset -> int -> tactic
-SIMPSET                : (simpset -> tactic) -> tactic
-SIMPSET'               : (simpset -> 'a -> tactic) -> 'a -> tactic
 \end{ttbox}
 
 These are the basic tactics that are underlying any actual
 simplification work.  The rewriting strategy is always strictly bottom
 up, except for congruence rules, which are applied while descending

   \texttt{asm_full_simp_tac}, but uses the safe solver as explained in
   \S\ref{sec:simp-solver}.  This tactic is mainly intended for
   building special tools, e.g.\ for combining the simplifier with the
   classical reasoner.  It is rarely used directly.
   
-\item[\ttindexbold{SIMPSET} $tacf$, \ttindexbold{SIMPSET'} $tacf'$]
-  are tacticals that make a tactic depend on the implicit current
-  simpset of the theory associated with the proof state they are
-  applied on.
-
 \end{ttdescription}
 
 \medskip
 
 Local modifications of simpsets within a proof are often much cleaner

 \S\ref{sec:simp-for-dummies}) should be considered harmful outside of
 actual proof scripts.  In particular, ML programs like theory
 definition packages or special tactics should refer to simpsets only
 explicitly, via the above tactics used in conjunction with
 \texttt{simpset_of} or the \texttt{SIMPSET} tacticals.
-
-\begin{warn}
-  There is a subtle difference between \texttt{(SIMPSET'~$tacf$)} and
-  \texttt{($tacf$~(simpset()))}.  For example \texttt{(SIMPSET'
-    simp_tac)} would depend on the theory of the proof state it is
-  applied to, while \texttt{(simp_tac (simpset()))} implicitly refers
-  to the current theory context.  Both are usually the same in proof
-  scripts, provided that goals are only stated within the current
-  theory.  Robust programs would not count on that, of course.
-\end{warn}
 
 
 \section{Forward rules and conversions}
 \index{simplification!forward rules}\index{simplification!conversions}
 \begin{ttbox}\index{*simplify}\index{*asm_simplify}\index{*full_simplify}\index{*asm_full_simplify}\index{*Simplifier.rewrite}\index{*Simplifier.asm_rewrite}\index{*Simplifier.full_rewrite}\index{*Simplifier.asm_full_rewrite}