--- a/doc-src/TutorialI/Misc/document/simp.tex Sat Mar 27 18:12:02 2010 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex Sat Mar 27 18:43:11 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%
%
--- a/doc-src/TutorialI/Misc/simp.thy Sat Mar 27 18:12:02 2010 +0100
+++ b/doc-src/TutorialI/Misc/simp.thy Sat Mar 27 18:43:11 2010 +0100
@@ -408,13 +408,22 @@
(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.
+ *}
subsection{*Finding Theorems\label{sec:find}*}