\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}\ {\isachardoublequote}set\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline
\isacommand{lemma}\ {\isachardoublequote}rev\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}%
\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 be 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}\ {\isachardoublequote}reset\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline
\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: