equal
deleted
inserted
replaced
29 ?x3 \# ?t3 = ?t3 == False |
29 ?x3 \# ?t3 = ?t3 == False |
30 Rewriting: |
30 Rewriting: |
31 [x] = [] == False |
31 [x] = [] == False |
32 \end{ttbox} |
32 \end{ttbox} |
33 |
33 |
34 In more complicated cases, the trace can quite lenghty, especially since |
34 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 |
35 invocations of the simplifier are often nested (e.g.\ when solving conditions |
36 of rewrite rules). Thus it is advisable to reset it:% |
36 of rewrite rules). Thus it is advisable to reset it:% |
37 \end{isamarkuptxt}% |
37 \end{isamarkuptxt}% |
38 \isacommand{ML}~{"}reset~trace\_simp{"}\isanewline |
38 \isacommand{ML}~{"}reset~trace\_simp{"}\isanewline |
39 \end{isabelle}% |
39 \end{isabelle}% |