doc-src/TutorialI/Inductive/inductive.tex
changeset 10520 bb9dfcc87951
parent 10468 87dda999deca
child 10762 cd1a2bee5549
     1.1 --- a/doc-src/TutorialI/Inductive/inductive.tex	Fri Nov 24 16:49:27 2000 +0100
     1.2 +++ b/doc-src/TutorialI/Inductive/inductive.tex	Sun Nov 26 10:48:38 2000 +0100
     1.3 @@ -15,10 +15,11 @@
     1.4  
     1.5  \input{Inductive/Even}
     1.6  \input{Inductive/document/Star}
     1.7 -\input{Inductive/document/AB}
     1.8  
     1.9  \section{Advanced inductive definitions}
    1.10  \input{Inductive/Advanced}
    1.11  
    1.12 +\input{Inductive/document/AB}
    1.13 +
    1.14  \index{inductive definition|)}
    1.15  \index{*inductive|)}