diff -r b2d1b393b750 -r 315afa77adea doc-src/TutorialI/appendix.tex
--- a/doc-src/TutorialI/appendix.tex	Mon Dec 04 23:38:19 2000 +0100
+++ b/doc-src/TutorialI/appendix.tex	Tue Dec 05 08:22:49 2000 +0100
@@ -58,6 +58,9 @@
 \indexboldpos{\isasymcirc}{$HOL1} &
 \ttindexbold{o} &
 \verb$\<circ>$\\
+\indexboldpos{\isasymbar~\isasymbar}{$HOL2arithfun}&
+\ttindexbold{abs}&
+\verb$\<bar> \<bar>$\\
 \indexboldpos{\isasymle}{$HOL2arithrel}&
 \ttindexboldpos{<=}{$HOL2arithrel}&
 \verb$\<le>$\\