# HG changeset patch
# User nipkow
# Date 976000969 -3600
# Node ID 315afa77adeac01335060b6d889544eac9e7cf4a
# Parent  b2d1b393b750fdc5c93f2d605cc928cfc3b0a086
*** empty log message ***

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>$\\