doc-src/TutorialI/appendix.tex

--- a/doc-src/TutorialI/appendix.tex	Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/appendix.tex	Tue Sep 12 15:43:15 2000 +0200
@@ -55,7 +55,7 @@
 \hline\hline
 \indexboldpos{\isasymcirc}{$HOL1} &
 \indexboldpos{\isasymle}{$HOL2arithrel}&
-&
+\indexboldpos{\isasymtimes}{$IsaFun}&
 &
 &
 &
@@ -66,7 +66,7 @@
  \\
 \ttindexbold{o} &
 \ttindexboldpos{<=}{$HOL2arithrel}&
-&
+\ttindexboldpos{*}{$HOL2arithfun} &
 &
 &
 &