# HG changeset patch
# User lcp
# Date 789958843 -3600
# Node ID 28a593f4b600dd9b9b9b7c1f101419bd517844f0
# Parent  c8e93e8b3f5547ee1889df2b75b90da02e11d7e6
Corrected indexing of *datatype

diff -r c8e93e8b3f55 -r 28a593f4b600 doc-src/Logics/Old_HOL.tex
--- 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}