diff options
Diffstat (limited to 'doc/refman/RefMan-tac.tex')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index a29dcbfd8..f62412f8f 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3323,6 +3323,24 @@ general principle of mutual induction for objects in type {\term$_i$}. \SeeAlso Section~\ref{Scheme-examples} +\subsection{\tt Combined Scheme\label{CombinedScheme} +\comindex{Combined Scheme}} +The {\tt Combined Scheme} command is a tool for combining +induction principles generated by the {\tt Scheme} command. +Its syntax follows the schema : + +\noindent +{\tt Combined Scheme {\ident$_0$} from {\ident$_1$}, .., {\ident$_n$}}\\ +\ident$_1$ \ldots \ident$_n$ are different inductive principles that must belong to +the same package of mutual inductive principle definitions. This command +generates {\ident$_0$} to be the conjunction of the principles: it is +built from the common premises of the principles and concluded by the +conjunction of their conclusions. + +\SeeAlso \ref{CombinedScheme-examples} + +\SeeAlso Section~\ref{CombinedScheme-examples} + \section{Generation of induction principles with {\tt Functional Scheme} \label{FunScheme} \comindex{Functional Scheme}} |