From df78c17c0d1545f2ce37b6c2bb3521f0d2fb130b Mon Sep 17 00:00:00 2001 From: msozeau Date: Sat, 23 Dec 2006 19:20:08 +0000 Subject: Doc for Combined Scheme. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9462 85f007b7-540e-0410-9357-904b9bb8a0f7 --- doc/refman/RefMan-tac.tex | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'doc/refman/RefMan-tac.tex') 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}} -- cgit v1.2.3