doc-src/TutorialI/appendix.tex
changeset 9933 9feb1e0c4cb3
parent 9541 d17c0b34d5c8
child 10171 59d6633835fa
     1.1 --- a/doc-src/TutorialI/appendix.tex	Tue Sep 12 14:59:44 2000 +0200
     1.2 +++ b/doc-src/TutorialI/appendix.tex	Tue Sep 12 15:43:15 2000 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4  \hline\hline
     1.5  \indexboldpos{\isasymcirc}{$HOL1} &
     1.6  \indexboldpos{\isasymle}{$HOL2arithrel}&
     1.7 -&
     1.8 +\indexboldpos{\isasymtimes}{$IsaFun}&
     1.9  &
    1.10  &
    1.11  &
    1.12 @@ -66,7 +66,7 @@
    1.13   \\
    1.14  \ttindexbold{o} &
    1.15  \ttindexboldpos{<=}{$HOL2arithrel}&
    1.16 -&
    1.17 +\ttindexboldpos{*}{$HOL2arithfun} &
    1.18  &
    1.19  &
    1.20  &