equal
deleted
inserted
replaced
1 (*<*)theory WFrec = Main:(*>*) |
1 (*<*)theory WFrec imports Main begin(*>*) |
2 |
2 |
3 text{*\noindent |
3 text{*\noindent |
4 So far, all recursive definitions were shown to terminate via measure |
4 So far, all recursive definitions were shown to terminate via measure |
5 functions. Sometimes this can be inconvenient or |
5 functions. Sometimes this can be inconvenient or |
6 impossible. Fortunately, \isacommand{recdef} supports much more |
6 impossible. Fortunately, \isacommand{recdef} supports much more |