equal
deleted
inserted
replaced
1663 The datatype \isa{term}, which is defined by |
1663 The datatype \isa{term}, which is defined by |
1664 \begin{alltt*}\isastyleminor |
1664 \begin{alltt*}\isastyleminor |
1665 consts term :: "i=>i" |
1665 consts term :: "i=>i" |
1666 datatype "term(A)" = Apply ("a \isasymin A", "l \isasymin list(term(A))") |
1666 datatype "term(A)" = Apply ("a \isasymin A", "l \isasymin list(term(A))") |
1667 monos list_mono |
1667 monos list_mono |
|
1668 type_elims list_univ [THEN subsetD, elim_format] |
1668 \end{alltt*} |
1669 \end{alltt*} |
1669 is an example of nested recursion. (The theorem \isa{list_mono} is proved |
1670 is an example of nested recursion. (The theorem \isa{list_mono} is proved |
1670 in theory \isa{List}, and the \isa{term} example is developed in |
1671 in theory \isa{List}, and the \isa{term} example is developed in |
1671 theory |
1672 theory |
1672 \thydx{Induct/Term}.) |
1673 \thydx{Induct/Term}.) |