1.1 --- a/doc-src/TutorialI/Misc/document/simp.tex	Sat Mar 27 18:12:02 2010 +0100
     1.2 +++ b/doc-src/TutorialI/Misc/document/simp.tex	Sat Mar 27 18:43:11 2010 +0100
     1.3 @@ -653,13 +653,21 @@
     1.4  (recursive!) simplification of the conditions, the latter prefixed by
     1.5  \texttt{[}$i+1$\texttt{]} instead of \texttt{[}$i$\texttt{]}.
     1.6  Another source of recursive invocations of the simplifier are
     1.7 -proofs of arithmetic formulae.
     1.8 +proofs of arithmetic formulae. By default, recursive invocations are not shown,
     1.9 +you must increase the trace depth via \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$ \pgmenu{Trace Simplifier Depth}.
    1.10  
    1.11  Many other hints about the simplifier's actions may appear.
    1.12  
    1.13  In more complicated cases, the trace can be very lengthy.  Thus it is
    1.14  advisable to reset the \pgmenu{Trace Simplifier} flag after having
    1.15 -obtained the desired trace.%
    1.16 +obtained the desired trace.
    1.17 +% Since this is easily forgotten (and may have the unpleasant effect of
    1.18 +% swamping the interface with trace information), here is how you can switch
    1.19 +% the trace on locally: * }
    1.20 +%
    1.21 +%using [[trace_simp=true]] apply(simp)
    1.22 +% In fact, any proof step can be prefixed with this \isa{using} clause,
    1.23 +% causing any local simplification to be traced.%
    1.24  \end{isamarkuptext}%
    1.25  \isamarkuptrue%
    1.26  %

     2.1 --- a/doc-src/TutorialI/Misc/simp.thy	Sat Mar 27 18:12:02 2010 +0100
     2.2 +++ b/doc-src/TutorialI/Misc/simp.thy	Sat Mar 27 18:43:11 2010 +0100
     2.3 @@ -408,13 +408,22 @@
     2.4  (recursive!) simplification of the conditions, the latter prefixed by
     2.5  \texttt{[}$i+1$\texttt{]} instead of \texttt{[}$i$\texttt{]}.
     2.6  Another source of recursive invocations of the simplifier are
     2.7 -proofs of arithmetic formulae.
     2.8 +proofs of arithmetic formulae. By default, recursive invocations are not shown,
     2.9 +you must increase the trace depth via \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$ \pgmenu{Trace Simplifier Depth}.
    2.10  
    2.11  Many other hints about the simplifier's actions may appear.
    2.12  
    2.13  In more complicated cases, the trace can be very lengthy.  Thus it is
    2.14  advisable to reset the \pgmenu{Trace Simplifier} flag after having
    2.15 -obtained the desired trace.  *}
    2.16 +obtained the desired trace.
    2.17 +% Since this is easily forgotten (and may have the unpleasant effect of
    2.18 +% swamping the interface with trace information), here is how you can switch
    2.19 +% the trace on locally: * }
    2.20 +%
    2.21 +%using [[trace_simp=true]] apply(simp)
    2.22 +% In fact, any proof step can be prefixed with this \isa{using} clause,
    2.23 +% causing any local simplification to be traced.
    2.24 + *}
    2.25  
    2.26  subsection{*Finding Theorems\label{sec:find}*}
    2.27