# HG changeset patch
# User wenzelm
# Date 1008084164 -3600
# Node ID 79b188f6d0aea72d3dca571acaa0804e8f5c127d
# Parent  b5630a4ea5d8ee7f73c4d8eb6d5d21a18606826c
\isasymindex made text mode;

diff -r b5630a4ea5d8 -r 79b188f6d0ae lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Tue Dec 11 16:22:09 2001 +0100
+++ b/lib/texinputs/isabellesym.sty	Tue Dec 11 16:22:44 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{~~}}