equal
deleted
inserted
replaced
1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Induction}% |
3 % |
4 % |
4 \begin{isamarkuptext}% |
5 \begin{isamarkuptext}% |
5 Assuming we have defined our function such that Isabelle could prove |
6 Assuming we have defined our function such that Isabelle could prove |
6 termination and that the recursion equations (or some suitable derived |
7 termination and that the recursion equations (or some suitable derived |
7 equations) are simplification rules, we might like to prove something about |
8 equations) are simplification rules, we might like to prove something about |