equal
deleted
inserted
replaced
1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 % |
3 % |
4 \begin{isamarkuptext}% |
4 \begin{isamarkuptext}% |
5 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 |
6 \ttindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going |
6 \isaindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going |
7 on:% |
7 on:% |
8 \end{isamarkuptext}% |
8 \end{isamarkuptext}% |
9 \isacommand{ML}\ {\isachardoublequote}set\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline |
9 \isacommand{ML}\ {\isachardoublequote}set\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline |
10 \isacommand{lemma}\ {\isachardoublequote}rev\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline |
10 \isacommand{lemma}\ {\isachardoublequote}rev\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline |
11 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}% |
11 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}% |