changeset 861 | 28a593f4b600 |
parent 841 | 14b96e3bd4ab |
child 1086 | 46a7b619e62e |
1.1 --- a/doc-src/Logics/Old_HOL.tex Thu Jan 12 10:53:42 1995 +0100 1.2 +++ b/doc-src/Logics/Old_HOL.tex Fri Jan 13 02:00:43 1995 +0100 1.3 @@ -1557,6 +1557,7 @@ 1.4 1.5 \index{primitive recursion|)} 1.6 \index{*primrec|)} 1.7 +\index{*datatype|)} 1.8 1.9 1.10 \section{Inductive and coinductive definitions}