discontinued default rendering for Oheimb's double-space;

--- 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\,}}