doc-src/TutorialI/Inductive/inductive.tex
changeset 48536 4e2ee88276d2
parent 48522 708278fc2dff
equal deleted inserted replaced
48535:619531d87ce4 48536:4e2ee88276d2
    16 \begin{warn}
    16 \begin{warn}
    17 Predicates can also be defined inductively.
    17 Predicates can also be defined inductively.
    18 See {\S}\ref{sec:ind-predicates}.
    18 See {\S}\ref{sec:ind-predicates}.
    19 \end{warn}
    19 \end{warn}
    20 
    20 
    21 \input{Inductive/document/Even}
    21 \input{document/Even}
    22 \input{Inductive/document/Mutual}
    22 \input{document/Mutual}
    23 \input{Inductive/document/Star}
    23 \input{document/Star}
    24 
    24 
    25 \section{Advanced Inductive Definitions}
    25 \section{Advanced Inductive Definitions}
    26 \label{sec:adv-ind-def}
    26 \label{sec:adv-ind-def}
    27 \input{Inductive/document/Advanced}
    27 \input{document/Advanced}
    28 
    28 
    29 \input{Inductive/document/AB}
    29 \input{document/AB}
    30 
    30 
    31 \index{inductive definitions|)}
    31 \index{inductive definitions|)}