equal
deleted
inserted
replaced
56 recdef with nested recursion: either an example or at least a pointer to the |
56 recdef with nested recursion: either an example or at least a pointer to the |
57 literature. In Recdef/termination.thy, at the end. |
57 literature. In Recdef/termination.thy, at the end. |
58 %FIXME, with one exception: nested recursion. |
58 %FIXME, with one exception: nested recursion. |
59 |
59 |
60 Syntax section: syntax annotations nor just for consts but also for constdefs and datatype. |
60 Syntax section: syntax annotations nor just for consts but also for constdefs and datatype. |
|
61 |
|
62 Appendix with list functions. |
61 |
63 |
62 |
64 |
63 Minor additions to the tutorial, unclear where |
65 Minor additions to the tutorial, unclear where |
64 ============================================== |
66 ============================================== |
65 |
67 |