changeset 10654 | 458068404143 |
parent 10420 | ef006735bee8 |
child 10885 | 90695f46440b |
--- a/doc-src/TutorialI/Misc/AdvancedInd.thy Wed Dec 13 09:32:55 2000 +0100 +++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Wed Dec 13 09:39:53 2000 +0100 @@ -290,8 +290,5 @@ example theorem @{thm[source]nat_less_induct} can be viewed (and derived) as a special case of @{thm[source]wf_induct} where @{term r} is @{text"<"} on @{typ nat}. The details can be found in the HOL library. -*}; - -(*<*) -end -(*>*) +*} +(*<*)end(*>*)