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