# HG changeset patch
# User wenzelm
# Date 940616653 -7200
# Node ID 1ee85d4205b2c86f3fec7f16d166eaed793657df
# Parent  35c18affc1d8b97e79461bdf65fe2284223b4319
new flag debug_simp

diff -r 35c18affc1d8 -r 1ee85d4205b2 doc-src/Ref/simplifier.tex
--- a/doc-src/Ref/simplifier.tex	Fri Oct 22 20:24:08 1999 +0200
+++ b/doc-src/Ref/simplifier.tex	Fri Oct 22 20:24:13 1999 +0200
@@ -39,6 +39,7 @@
 Full_simp_tac     : int -> tactic
 Asm_full_simp_tac : int -> tactic
 trace_simp        : bool ref \hfill{\bf initially false}
+debug_simp        : bool ref \hfill{\bf initially false}
 \end{ttbox}
 
 \begin{ttdescription}
@@ -60,9 +61,12 @@
 \footnote{\texttt{Asm_full_simp_tac} used to process the assumptions from
   left to right. For backwards compatibilty reasons only there is now
   \texttt{Asm_lr_simp_tac} that behaves like the old \texttt{Asm_full_simp_tac}.}
-\item[set \ttindexbold{trace_simp};] makes the simplifier output
-  internal operations.  This includes rewrite steps, but also
-  bookkeeping like modifications of the simpset.
+\item[set \ttindexbold{trace_simp};] makes the simplifier output internal
+  operations.  This includes rewrite steps, but also bookkeeping like
+  modifications of the simpset.
+\item[set \ttindexbold{debug_simp};] makes the simplifier output some extra
+  information about internal operations.  This includes any attempted
+  invocation of simplification procedures.
 \end{ttdescription}
 
 \medskip