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