doc-src/ind-defs.toc

added const_type: sg -> typ option;
stamps now stored in REVERSE order;
now supports 'draft signatures' and incremental extension: is_draft,
add_classes (supports axclasses), add_defsort, add_types, add_tyabbrs,
add_tyabbrs_i, add_arities, add_consts, add_consts_i, add_syntax,
add_syntax_i, add_trfuns, add_trrules, add_name, make_draft;
added const_of_class, class_of_const (for axclasses);
changed the pure signature to support axclasses (added itself, TYPE);
various major internal changes;

\contentsline {section}{\numberline {1}Introduction}{1}
\contentsline {section}{\numberline {2}Fixedpoint operators}{1}
\contentsline {section}{\numberline {3}Elements of an inductive or coinductive definition}{2}
\contentsline {subsection}{\numberline {3.1}The form of the introduction rules}{2}
\contentsline {subsection}{\numberline {3.2}The fixedpoint definitions}{3}
\contentsline {subsection}{\numberline {3.3}Mutual recursion}{3}
\contentsline {subsection}{\numberline {3.4}Proving the introduction rules}{4}
\contentsline {subsection}{\numberline {3.5}The elimination rule}{4}
\contentsline {section}{\numberline {4}Induction and coinduction rules}{4}
\contentsline {subsection}{\numberline {4.1}The basic induction rule}{4}
\contentsline {subsection}{\numberline {4.2}Mutual induction}{5}
\contentsline {subsection}{\numberline {4.3}Coinduction}{5}
\contentsline {section}{\numberline {5}Examples of inductive and coinductive definitions}{6}
\contentsline {subsection}{\numberline {5.1}The finite set operator}{6}
\contentsline {subsection}{\numberline {5.2}Lists of $n$ elements}{6}
\contentsline {subsection}{\numberline {5.3}A coinductive definition: bisimulations on lazy lists}{7}
\contentsline {subsection}{\numberline {5.4}The accessible part of a relation}{8}
\contentsline {subsection}{\numberline {5.5}The primitive recursive functions}{9}
\contentsline {section}{\numberline {6}Datatypes and codatatypes}{11}
\contentsline {subsection}{\numberline {6.1}Constructors and their domain}{11}
\contentsline {subsection}{\numberline {6.2}The case analysis operator}{11}
\contentsline {section}{\numberline {7}Conclusions and future work}{12}