doc-src/TutorialI/appendix.tex

 \ttindexbold{SOME} &
 \verb$\<epsilon>$\\
 \indexboldpos{\isasymcirc}{$HOL1} &
 \ttindexbold{o} &
 \verb$\<circ>$\\
+\indexboldpos{\isasymbar~\isasymbar}{$HOL2arithfun}&
+\ttindexbold{abs}&
+\verb$\<bar> \<bar>$\\
 \indexboldpos{\isasymle}{$HOL2arithrel}&
 \ttindexboldpos{<=}{$HOL2arithrel}&
 \verb$\<le>$\\
 \indexboldpos{\isasymtimes}{$Isatype}&
 \ttindexboldpos{*}{$HOL2arithfun} &