doc-src/TutorialI/Inductive/inductive.tex
changeset 49537 708278fc2dff
parent 25330 15bf0f47a87d
     1.1 --- a/doc-src/TutorialI/Inductive/inductive.tex	Thu Jul 26 17:32:28 2012 +0200
     1.2 +++ b/doc-src/TutorialI/Inductive/inductive.tex	Thu Jul 26 18:55:42 2012 +0200
     1.3 @@ -18,14 +18,14 @@
     1.4  See {\S}\ref{sec:ind-predicates}.
     1.5  \end{warn}
     1.6  
     1.7 -\input{Inductive/document/Even}
     1.8 -\input{Inductive/document/Mutual}
     1.9 -\input{Inductive/document/Star}
    1.10 +\input{document/Even}
    1.11 +\input{document/Mutual}
    1.12 +\input{document/Star}
    1.13  
    1.14  \section{Advanced Inductive Definitions}
    1.15  \label{sec:adv-ind-def}
    1.16 -\input{Inductive/document/Advanced}
    1.17 +\input{document/Advanced}
    1.18  
    1.19 -\input{Inductive/document/AB}
    1.20 +\input{document/AB}
    1.21  
    1.22  \index{inductive definitions|)}