# HG changeset patch
# User oheimb
# Date 888574696 -3600
# Node ID 05d33fc7aa0811eaa27f3bd9331c0c47919fc9df
# Parent  27fa93c22b9b58c7da04001341b0d968e2481556
added minimal description of rep_ss

diff -r 27fa93c22b9b -r 05d33fc7aa08 doc-src/Ref/simplifier.tex
--- a/doc-src/Ref/simplifier.tex	Fri Feb 27 11:08:20 1998 +0100
+++ b/doc-src/Ref/simplifier.tex	Fri Feb 27 11:18:16 1998 +0100
@@ -208,6 +208,11 @@
 \subsection{Inspecting simpsets}
 \begin{ttbox}
 print_ss : simpset -> unit
+rep_ss   : simpset -> {mss        : meta_simpset, 
+                       subgoal_tac: simpset  -> int -> tactic,
+                       loop_tac   :             int -> tactic,
+                       finish_tac : thm list -> int -> tactic,
+                unsafe_finish_tac : thm list -> int -> tactic}
 \end{ttbox}
 \begin{ttdescription}
   
@@ -218,6 +223,10 @@
   also shown.  The other parts, functions and tactics, are
   non-printable.
 
+\item[\ttindexbold{rep_ss} $ss$;] decomposes $ss$ as a record of its internal 
+  components, namely the meta_simpset, the subgoaler, the loop, and the safe
+  and unsafe solvers.
+
 \end{ttdescription}