# HG changeset patch
# User nipkow
# Date 1269711791 -3600
# Node ID 380b974967343a0c5c55d87752c649d9cdfc710a
# Parent  6ba5526588072325330c859cc5ca0c33c93e5759# Parent  78674c6018ca4e91c896bed80c984816a9be1682
merged

diff -r 6ba552658807 -r 380b97496734 doc-src/TutorialI/Misc/document/simp.tex
--- 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%
 %
diff -r 6ba552658807 -r 380b97496734 doc-src/TutorialI/Misc/simp.thy
--- 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}*}