*** empty log message ***
authornipkow
Tue Dec 05 08:22:49 2000 +0100 (2000-12-05)
changeset 10590315afa77adea
parent 10589 b2d1b393b750
child 10591 6d6cb845e841
*** empty log message ***
doc-src/TutorialI/appendix.tex
     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>$\\