| changeset 17914 | 99ead7a7eb42 |
| parent 13111 | 2d6782e71702 |
| child 20217 | 25b068a99d2b |
--- a/doc-src/TutorialI/Advanced/WFrec.thy Wed Oct 19 17:21:53 2005 +0200 +++ b/doc-src/TutorialI/Advanced/WFrec.thy Wed Oct 19 21:52:07 2005 +0200 @@ -1,4 +1,4 @@ -(*<*)theory WFrec = Main:(*>*) +(*<*)theory WFrec imports Main begin(*>*) text{*\noindent So far, all recursive definitions were shown to terminate via measure