doc-src/HOL/HOL.tex
changeset 12180 91c9f661b183
parent 11242 81fe09ce5fc9
child 12611 c44a9fecb518
     1.1 --- a/doc-src/HOL/HOL.tex	Wed Nov 14 18:42:34 2001 +0100
     1.2 +++ b/doc-src/HOL/HOL.tex	Wed Nov 14 18:44:27 2001 +0100
     1.3 @@ -2915,13 +2915,12 @@
     1.4  inductive    {\it inductive sets}
     1.5    intrs      {\it introduction rules}
     1.6    monos      {\it monotonicity theorems}
     1.7 -  con_defs   {\it constructor definitions}
     1.8  \end{ttbox}
     1.9  A coinductive definition is identical, except that it starts with the keyword
    1.10  \texttt{coinductive}.  
    1.11  
    1.12 -The \texttt{monos} and \texttt{con_defs} sections are optional.  If present,
    1.13 -each is specified by a list of identifiers.
    1.14 +The \texttt{monos} section is optional; if present it is specified by a list
    1.15 +of identifiers.
    1.16  
    1.17  \begin{itemize}
    1.18  \item The \textit{inductive sets} are specified by one or more strings.