equal
deleted
inserted
replaced
1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{termination}% |
3 % |
4 % |
4 \begin{isamarkuptext}% |
5 \begin{isamarkuptext}% |
5 When a function is defined via \isacommand{recdef}, Isabelle tries to prove |
6 When a function is defined via \isacommand{recdef}, Isabelle tries to prove |
6 its termination with the help of the user-supplied measure. All of the above |
7 its termination with the help of the user-supplied measure. All of the above |
7 examples are simple enough that Isabelle can prove automatically that the |
8 examples are simple enough that Isabelle can prove automatically that the |