equal
deleted
inserted
replaced
2 theory trace_simp = Main:; |
2 theory trace_simp = Main:; |
3 (*>*) |
3 (*>*) |
4 |
4 |
5 text{* |
5 text{* |
6 Using the simplifier effectively may take a bit of experimentation. Set the |
6 Using the simplifier effectively may take a bit of experimentation. Set the |
7 \ttindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going |
7 \isaindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going |
8 on: |
8 on: |
9 *} |
9 *} |
10 ML "set trace_simp"; |
10 ML "set trace_simp"; |
11 lemma "rev [a] = []"; |
11 lemma "rev [a] = []"; |
12 apply(simp); |
12 apply(simp); |