doc-src/Ref/simplifier.tex

 
 \end{ttdescription}
 
 
 \subsection{Accessing the current simpset}
-
-\begin{ttbox}
-simpset        : unit -> simpset
-simpset_ref    : unit -> simpset ref
+\label{sec:access-current-simpset}
+
+\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
+SIMPSET        :(simpset ->       tactic) ->       tactic
+SIMPSET'       :(simpset -> 'a -> tactic) -> 'a -> tactic
 \end{ttbox}
 
 Each theory contains a current simpset\index{simpset!current} stored
 within a private ML reference variable.  This can be retrieved and
 modified as follows.

 \item[\ttindexbold{simpset_of} $thy$;] retrieves the simpset value
   from theory $thy$.
   
 \item[\ttindexbold{simpset_ref_of} $thy$;] retrieves the simpset
   reference variable from theory $thy$.
+
+\item[\ttindexbold{print_simpset} $thy$;] prints the current simpset
+  of theory $thy$ in the same way as \texttt{print_ss}.
 
 \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