--- 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}