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}