doc-src/TutorialI/Inductive/inductive.tex
changeset 10468 87dda999deca
parent 10371 4015fdd0bcf0
child 10520 bb9dfcc87951
equal deleted inserted replaced
10467:e6e7205e9e91 10468:87dda999deca
    16 \input{Inductive/Even}
    16 \input{Inductive/Even}
    17 \input{Inductive/document/Star}
    17 \input{Inductive/document/Star}
    18 \input{Inductive/document/AB}
    18 \input{Inductive/document/AB}
    19 
    19 
    20 \section{Advanced inductive definitions}
    20 \section{Advanced inductive definitions}
    21 \input{Inductive/document/Advanced}
    21 \input{Inductive/Advanced}
    22 
    22 
    23 \index{inductive definition|)}
    23 \index{inductive definition|)}
    24 \index{*inductive|)}
    24 \index{*inductive|)}