equal
deleted
inserted
replaced
1 \begin{isabelle}% |
1 % |
|
2 \begin{isabellebody}% |
2 % |
3 % |
3 \begin{isamarkuptext}% |
4 \begin{isamarkuptext}% |
4 Using the simplifier effectively may take a bit of experimentation. Set the |
5 Using the simplifier effectively may take a bit of experimentation. Set the |
5 \ttindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going |
6 \ttindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going |
6 on:% |
7 on:% |
34 In more complicated cases, the trace can be quite lenghty, especially since |
35 In more complicated cases, the trace can be quite lenghty, especially since |
35 invocations of the simplifier are often nested (e.g.\ when solving conditions |
36 invocations of the simplifier are often nested (e.g.\ when solving conditions |
36 of rewrite rules). Thus it is advisable to reset it:% |
37 of rewrite rules). Thus it is advisable to reset it:% |
37 \end{isamarkuptxt}% |
38 \end{isamarkuptxt}% |
38 \isacommand{ML}\ {\isachardoublequote}reset\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline |
39 \isacommand{ML}\ {\isachardoublequote}reset\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline |
39 \end{isabelle}% |
40 \end{isabellebody}% |
40 %%% Local Variables: |
41 %%% Local Variables: |
41 %%% mode: latex |
42 %%% mode: latex |
42 %%% TeX-master: "root" |
43 %%% TeX-master: "root" |
43 %%% End: |
44 %%% End: |