diff -r cb9d47632573 -r 2665170f104a doc-src/TutorialI/Misc/document/trace_simp.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/document/trace_simp.tex	Wed Apr 19 12:59:38 2000 +0200
@@ -0,0 +1,39 @@
+\begin{isabelle}%
+%
+\begin{isamarkuptext}%
+Using the simplifier effectively may take a bit of experimentation.  Set the
+\ttindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going
+on:%
+\end{isamarkuptext}%
+\isacommand{ML}~{"}set~trace\_simp{"}\isanewline
+\isacommand{lemma}~{"}rev~[a]~=~[]{"}\isanewline
+\isacommand{apply}(simp)%
+\begin{isamarkuptxt}%
+\noindent
+produces the trace
+
+\begin{ttbox}
+Applying instance of rewrite rule:
+rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1]
+Rewriting:
+rev [x] == rev [] @ [x]
+Applying instance of rewrite rule:
+rev [] == []
+Rewriting:
+rev [] == []
+Applying instance of rewrite rule:
+[] @ ?y == ?y
+Rewriting:
+[] @ [x] == [x]
+Applying instance of rewrite rule:
+?x3 \# ?t3 = ?t3 == False
+Rewriting:
+[x] = [] == False
+\end{ttbox}
+
+In more complicated cases, the trace can quite lenghty, especially since
+invocations of the simplifier are often nested (e.g.\ when solving conditions
+of rewrite rules). Thus it is advisable to reset it:%
+\end{isamarkuptxt}%
+\isacommand{ML}~{"}reset~trace\_simp{"}\isanewline
+\end{isabelle}%