1.1 --- a/doc-src/TutorialI/appendix.tex	Mon Dec 04 23:38:19 2000 +0100
     1.2 +++ b/doc-src/TutorialI/appendix.tex	Tue Dec 05 08:22:49 2000 +0100
     1.3 @@ -58,6 +58,9 @@
     1.4  \indexboldpos{\isasymcirc}{$HOL1} &
     1.5  \ttindexbold{o} &
     1.6  \verb$\<circ>$\\
     1.7 +\indexboldpos{\isasymbar~\isasymbar}{$HOL2arithfun}&
     1.8 +\ttindexbold{abs}&
     1.9 +\verb$\<bar> \<bar>$\\
    1.10  \indexboldpos{\isasymle}{$HOL2arithrel}&
    1.11  \ttindexboldpos{<=}{$HOL2arithrel}&
    1.12  \verb$\<le>$\\