# HG changeset patch
# User nipkow
# Date 1269848841 -7200
# Node ID a15454b23ebd86977db145b62d272a4eeb286839
# Parent  3956a7636d5de10e1d90d5b1b28850622c3b2318
documented [[trace_simp=true]]

diff -r 3956a7636d5d -r a15454b23ebd doc-src/TutorialI/Misc/document/simp.tex
--- a/doc-src/TutorialI/Misc/document/simp.tex	Sun Mar 28 19:34:08 2010 +0200
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Mon Mar 29 09:47:21 2010 +0200
@@ -661,13 +661,33 @@
 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.
-% 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: * }
+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 in a proof:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimproof
+%
+\endisadelimproof
 %
-%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.%
+\isatagproof
+\isacommand{using}\isamarkupfalse%
+\ {\isacharbrackleft}{\isacharbrackleft}trace{\isacharunderscore}simp{\isacharequal}true{\isacharbrackright}{\isacharbrackright}\isanewline
+\isacommand{apply}\isamarkupfalse%
+\ simp%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent
+Within the current proof, all simplifications in subsequent proof steps
+will be traced, but the text reminds you to remove the \isa{using} clause
+after it has done its job.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r 3956a7636d5d -r a15454b23ebd doc-src/TutorialI/Misc/simp.thy
--- a/doc-src/TutorialI/Misc/simp.thy	Sun Mar 28 19:34:08 2010 +0200
+++ b/doc-src/TutorialI/Misc/simp.thy	Mon Mar 29 09:47:21 2010 +0200
@@ -416,14 +416,20 @@
 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.
-% 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.
- *}
+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 in a proof: *}
+
+(*<*)lemma "x=x"
+(*>*)
+using [[trace_simp=true]]
+apply simp
+(*<*)oops(*>*)
+
+text{* \noindent
+Within the current proof, all simplifications in subsequent proof steps
+will be traced, but the text reminds you to remove the \isa{using} clause
+after it has done its job. *}
 
 subsection{*Finding Theorems\label{sec:find}*}