# HG changeset patch
# User wenzelm
# Date 1326554754 -3600
# Node ID 0a5af667dc75a6d856680d6bdd3e9361c65e71f4
# Parent  d86ef6b960973ae007a2849e2c5f86e2f0cf881c
discontinued default rendering for Oheimb's double-space;

diff -r d86ef6b96097 -r 0a5af667dc75 etc/symbols
--- 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: =^
diff -r d86ef6b96097 -r 0a5af667dc75 lib/texinputs/isabellesym.sty
--- 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\,}}