doc-src/TutorialI/appendix.tex

--- a/doc-src/TutorialI/appendix.tex	Wed Nov 29 10:22:38 2000 +0100
+++ b/doc-src/TutorialI/appendix.tex	Wed Nov 29 13:44:26 2000 +0100
@@ -61,7 +61,7 @@
 \indexboldpos{\isasymle}{$HOL2arithrel}&
 \ttindexboldpos{<=}{$HOL2arithrel}&
 \verb$\<le>$\\
-\indexboldpos{\isasymtimes}{$IsaFun}&
+\indexboldpos{\isasymtimes}{$Isatype}&
 \ttindexboldpos{*}{$HOL2arithfun} &
 \verb$\<times>$\\
 \indexboldpos{\isasymin}{$HOL3Set0a}&