give equal credit to several originators of inductive schemas

Author: mikeshulman

induction.tex

@@ -1264,8 +1264,8 @@ \section{Identity types and identity systems}
 In type theory, particular cases of inductive definitions date back to Martin-L\"of's original papers: \cite{martin-lof-hauptsatz} presents a general notion of inductively defined predicates and relations; the notion of inductive type was present (but only with instances, not as a general notion) in Martin-L\"of's first papers in type theory \cite{Martin-Lof-1973};
 and then as a general notion with $\w$-types in \cite{Martin-Lof-1979}.\index{Martin-L\"of}%
 
-A general notion of inductive type was introduced in 1985 by Constable and Mendler~\cite{DBLP:conf/lop/ConstableM85}.  A general schema for inductive types in intensional type theory was suggested in
-\cite{PfenningPaulinMohring}.  Further developments included \cite{CoquandPaulin, Dybjer:1991}.
+A general notion of inductive type was introduced in 1985 by Constable and Mendler~\cite{DBLP:conf/lop/ConstableM85}.  General schemas for inductive types in intensional type theory were suggested in
+\cite{PfenningPaulinMohring, CoquandPaulin, Dybjer:1991}.
 
 The notion of inductive-recursive definition appears in \cite{Dybjer:2000}. An important  type-theoretic notion is the notion of tree types (a general expression of the notion of Post system in type theory) which appears in \cite{PeterssonSynek}.