diff -r 99bd3e902979 -r 4015fdd0bcf0 doc-src/TutorialI/Inductive/inductive.tex
--- a/doc-src/TutorialI/Inductive/inductive.tex	Fri Nov 03 10:24:33 2000 +0100
+++ b/doc-src/TutorialI/Inductive/inductive.tex	Fri Nov 03 10:26:23 2000 +0100
@@ -17,7 +17,8 @@
 \input{Inductive/document/Star}
 \input{Inductive/document/AB}
 
+\section{Advanced inductive definitions}
+\input{Inductive/document/Advanced}
+
 \index{inductive definition|)}
 \index{*inductive|)}
-
-\section{Advanced inductive definitions}