# HG changeset patch
# User oheimb
# Date 906731669 -7200
# Node ID 9ea449586464846f2b10e382dfa38f1e48b58e85
# Parent  620130d6b8e6c62e8713b6c9fddf5305208881a7
improved indentation

diff -r 620130d6b8e6 -r 9ea449586464 doc-src/Ref/simplifier.tex
--- a/doc-src/Ref/simplifier.tex	Fri Sep 25 15:21:07 1998 +0200
+++ b/doc-src/Ref/simplifier.tex	Fri Sep 25 15:54:29 1998 +0200
@@ -267,15 +267,16 @@
 
 
 \subsection{Accessing the current simpset}
+\label{sec:access-current-simpset}
 
 \begin{ttbox}
-simpset        : unit -> simpset
-simpset_ref    : unit -> simpset ref
+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
@@ -297,14 +298,14 @@
 \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}