doc-src/Inductive/ind-defs.bbl
changeset 4058 18fea4aa9625
parent 3162 78fa85d44e68
child 4585 9e7a32dfc1f2
equal deleted inserted replaced
4057:edd8cb346109 4058:18fea4aa9625
   123 Paulin-Mohring, C.,
   123 Paulin-Mohring, C.,
   124 \newblock Inductive definitions in the system {Coq}: Rules and properties,
   124 \newblock Inductive definitions in the system {Coq}: Rules and properties,
   125 \newblock In {\em Typed Lambda Calculi and Applications\/} (1993), M.~Bezem
   125 \newblock In {\em Typed Lambda Calculi and Applications\/} (1993), M.~Bezem
   126   J.~Groote, Eds., LNCS 664, Springer, pp.~328--345
   126   J.~Groote, Eds., LNCS 664, Springer, pp.~328--345
   127 
   127 
   128 \bibitem{paulson-markt}
       
   129 Paulson, L.~C.,
       
   130 \newblock Tool support for logics of programs,
       
   131 \newblock In {\em Mathematical Methods in Program Development: Summer School
       
   132   Marktoberdorf 1996}, M.~Broy, Ed., NATO ASI Series F. Springer,
       
   133 \newblock In press
       
   134 
       
   135 \bibitem{paulson87}
   128 \bibitem{paulson87}
   136 Paulson, L.~C.,
   129 Paulson, L.~C.,
   137 \newblock {\em Logic and Computation: Interactive proof with Cambridge LCF},
   130 \newblock {\em Logic and Computation: Interactive proof with Cambridge LCF},
   138 \newblock Cambridge Univ. Press, 1987
   131 \newblock Cambridge Univ. Press, 1987
   139 
   132 
   160 
   153 
   161 \bibitem{paulson-final}
   154 \bibitem{paulson-final}
   162 Paulson, L.~C.,
   155 Paulson, L.~C.,
   163 \newblock A concrete final coalgebra theorem for {ZF} set theory,
   156 \newblock A concrete final coalgebra theorem for {ZF} set theory,
   164 \newblock In Dybjer et~al. \cite{types94}, pp.~120--139
   157 \newblock In Dybjer et~al. \cite{types94}, pp.~120--139
       
   158 
       
   159 \bibitem{paulson-markt}
       
   160 Paulson, L.~C.,
       
   161 \newblock Tool support for logics of programs,
       
   162 \newblock In {\em Mathematical Methods in Program Development: Summer School
       
   163   Marktoberdorf 1996}, M.~Broy, Ed., NATO ASI Series F. Springer, Published
       
   164   1997,
       
   165 \newblock In press
   165 
   166 
   166 \bibitem{paulson-gr}
   167 \bibitem{paulson-gr}
   167 Paulson, L.~C., Gr\c{a}bczewski, K.,
   168 Paulson, L.~C., Gr\c{a}bczewski, K.,
   168 \newblock Mechanizing set theory: Cardinal arithmetic and the axiom of choice,
   169 \newblock Mechanizing set theory: Cardinal arithmetic and the axiom of choice,
   169 \newblock {\em J. Auto. Reas. {\bf 17}}, 3 (Dec. 1996), 291--323
   170 \newblock {\em J. Auto. Reas. {\bf 17}}, 3 (Dec. 1996), 291--323