--- a/doc-src/Logics/Old_HOL.tex Thu Jan 12 10:53:42 1995 +0100
+++ b/doc-src/Logics/Old_HOL.tex Fri Jan 13 02:00:43 1995 +0100
@@ -1557,6 +1557,7 @@
\index{primitive recursion|)}
\index{*primrec|)}
+\index{*datatype|)}
\section{Inductive and coinductive definitions}