doc-src/TutorialI/Misc/AdvancedInd.thy

--- 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(*>*)