--- a/doc-src/TutorialI/isabellesym.sty Thu Dec 13 17:57:55 2001 +0100
+++ b/doc-src/TutorialI/isabellesym.sty Thu Dec 13 19:05:10 2001 +0100
@@ -345,10 +345,10 @@
\newcommand{\isasymJoin}{\isamath{\Join}} %requires latexsym
\newcommand{\isasymwp}{\isamath{\wp}}
\newcommand{\isasymwrong}{\isamath{\wr}}
-\newcommand{\isasymspacespace}{\isamath{~~}}
+\newcommand{\isasymstruct}{\isamath{\diamond}}
\newcommand{\isasymacute}{\isatext{\'\relax}}
+\newcommand{\isasymindex}{\isatext{\i}}
\newcommand{\isasymdieresis}{\isatext{\"\relax}}
-\newcommand{\isasymstruct}{\isamath{\diamond}}
-\newcommand{\isasymindex}{\isamath{\i}}
\newcommand{\isasymcedilla}{\isatext{\c\relax}}
\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
+\newcommand{\isasymspacespace}{\isamath{~~}}