
diff -r 5ceedb86aa9d -r 78674c6018ca doc-src/TutorialI/Misc/document/simp.tex
--- a/doc-src/TutorialI/Misc/document/simp.tex	Sat Mar 27 14:48:46 2010 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Sat Mar 27 18:42:27 2010 +0100
@@ -653,13 +653,21 @@
 (recursive!) simplification of the conditions, the latter prefixed by
 \texttt{[}$i+1$\texttt{]} instead of \texttt{[}$i$\texttt{]}.
 Another source of recursive invocations of the simplifier are
-proofs of arithmetic formulae.
+proofs of arithmetic formulae. By default, recursive invocations are not shown,
+you must increase the trace depth via \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$ \pgmenu{Trace Simplifier Depth}.
 
 Many other hints about the simplifier's actions may appear.
 
 In more complicated cases, the trace can be very lengthy.  Thus it is
 advisable to reset the \pgmenu{Trace Simplifier} flag after having
-obtained the desired trace.%
+obtained the desired trace.
+% Since this is easily forgotten (and may have the unpleasant effect of
+% swamping the interface with trace information), here is how you can switch
+% the trace on locally: * }
+%
+%using [[trace_simp=true]] apply(simp)
+% In fact, any proof step can be prefixed with this \isa{using} clause,
+% causing any local simplification to be traced.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %




