--- a/etc/symbols Sat Jan 14 16:14:22 2012 +0100
+++ b/etc/symbols Sat Jan 14 16:25:54 2012 +0100
@@ -351,7 +351,6 @@
\<dieresis> code: 0x0000a8
\<cedilla> code: 0x0000b8
\<hungarumlaut> code: 0x0002dd
-\<spacespace> code: 0x002423
\<some> code: 0x0003f5
\<^sub> code: 0x0021e9 abbrev: =_
\<^sup> code: 0x0021e7 abbrev: =^
--- a/lib/texinputs/isabellesym.sty Sat Jan 14 16:14:22 2012 +0100
+++ b/lib/texinputs/isabellesym.sty Sat Jan 14 16:25:54 2012 +0100
@@ -353,8 +353,7 @@
\newcommand{\isasymdieresis}{\isatext{\"\relax}}
\newcommand{\isasymcedilla}{\isatext{\c\relax}}
\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
-\newcommand{\isasymspacespace}{\isamath{~~}}
\newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}
-\newcommand{\isasymsome}{\isamath{\epsilon\,}}
\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
\newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}}
+\newcommand{\isasymsome}{\isamath{\epsilon\,}}