diff options
| author | Hugo Herbelin | 2014-09-07 16:56:24 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-09-10 10:58:06 +0200 |
| commit | 47fc0cbd21c954dbed9ee021dbb7c54ac981d2d8 (patch) | |
| tree | 3819e36792c2b1016babafd82c85044c4787861d /doc | |
| parent | edfa5e986a25eb7a0719d20b43a618cb5bd4cd95 (diff) | |
Removing "eqn:" for "induction" in reference manual.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 2bbeb3b1ab..90055ea837 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1728,17 +1728,17 @@ induction n. {\tt (}$p_{1}$ {\tt ,} {\ldots} {\tt ,} $p_{n}${\tt )} can be used instead of {\tt [} $p_{1}$ {\ldots} $p_{n}$ {\tt ]}. -\item{\tt induction {\term} eqn:{\namingintropattern}} +%% \item{\tt induction {\term} eqn:{\namingintropattern}} - This behaves as {\tt induction {\term}} but adds an equation between - {\term} and the value that {\term} takes in each of the induction - case. The name of the equation is built according to - {\namingintropattern} which can be an identifier, a ``?'', etc, as - indicated in Section~\ref{intros-pattern}. +%% This behaves as {\tt induction {\term}} but adds an equation between +%% {\term} and the value that {\term} takes in each of the induction +%% case. The name of the equation is built according to +%% {\namingintropattern} which can be an identifier, a ``?'', etc, as +%% indicated in Section~\ref{intros-pattern}. -\item{\tt induction {\term} as {\disjconjintropattern} eqn:{\namingintropattern}} +%% \item{\tt induction {\term} as {\disjconjintropattern} eqn:{\namingintropattern}} - This combines the two previous forms. +%% This combines the two previous forms. \item{\tt induction {\term} with \bindinglist} @@ -1779,15 +1779,15 @@ induction n. Section~\ref{Occurrences clauses}. \item {\tt induction {\term$_1$} with {\bindinglist$_1$} - as {\disjconjintropattern} eqn:{\namingintropattern} + as {\disjconjintropattern} %% eqn:{\namingintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}\\ {\tt einduction {\term$_1$} with {\bindinglist$_1$} - as {\disjconjintropattern} eqn:{\namingintropattern} + as {\disjconjintropattern} %% eqn:{\namingintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}} These are the most general forms of {\tt induction} and {\tt - einduction}. It combines the effects of the {\tt with}, {\tt as}, - {\tt eqn:}, {\tt using}, and {\tt in} clauses. + einduction}. It combines the effects of the {\tt with}, {\tt as}, %%{\tt eqn:}, + {\tt using}, and {\tt in} clauses. \item{\tt induction !{\ident}} |