equal
deleted
inserted
replaced
1312 equality and run your tactic on the de Bruijn formulae discussed |
1312 equality and run your tactic on the de Bruijn formulae discussed |
1313 in Exercise~\ref{ex:debruijn}. |
1313 in Exercise~\ref{ex:debruijn}. |
1314 \end{exercise} |
1314 \end{exercise} |
1315 *} |
1315 *} |
1316 |
1316 |
1317 section {* Simplifier Tactics *} |
1317 section {* Simplifier Tactics\label{sec:simplifier} *} |
1318 |
1318 |
1319 text {* |
1319 text {* |
1320 A lot of convenience in reasoning with Isabelle derives from its |
1320 A lot of convenience in reasoning with Isabelle derives from its |
1321 powerful simplifier. We will describe it in this section. However, |
1321 powerful simplifier. We will describe it in this section. However, |
1322 due to its complexity, we can mostly only scratch the surface. |
1322 due to its complexity, we can mostly only scratch the surface. |