diff -r e6e7205e9e91 -r 87dda999deca doc-src/TutorialI/Inductive/inductive.tex --- a/doc-src/TutorialI/Inductive/inductive.tex Tue Nov 14 13:26:48 2000 +0100 +++ b/doc-src/TutorialI/Inductive/inductive.tex Tue Nov 14 17:02:36 2000 +0100 @@ -18,7 +18,7 @@ \input{Inductive/document/AB} \section{Advanced inductive definitions} -\input{Inductive/document/Advanced} +\input{Inductive/Advanced} \index{inductive definition|)} \index{*inductive|)}