doc-src/TutorialI/appendix.tex
changeset 10538 d1bf9ca9008d
parent 10328 bf33cbd76c05
child 10590 315afa77adea
     1.1 --- a/doc-src/TutorialI/appendix.tex	Wed Nov 29 10:22:38 2000 +0100
     1.2 +++ b/doc-src/TutorialI/appendix.tex	Wed Nov 29 13:44:26 2000 +0100
     1.3 @@ -61,7 +61,7 @@
     1.4  \indexboldpos{\isasymle}{$HOL2arithrel}&
     1.5  \ttindexboldpos{<=}{$HOL2arithrel}&
     1.6  \verb$\<le>$\\
     1.7 -\indexboldpos{\isasymtimes}{$IsaFun}&
     1.8 +\indexboldpos{\isasymtimes}{$Isatype}&
     1.9  \ttindexboldpos{*}{$HOL2arithfun} &
    1.10  \verb$\<times>$\\
    1.11  \indexboldpos{\isasymin}{$HOL3Set0a}&