prefer calligrapic \<RR> \<II> over \<Re> \<Im> for "screen" display (NB: official unicode defines only one version of these glyphs, unlike TeX);

--- a/etc/symbols	Fri Aug 03 17:56:35 2012 +0200
+++ b/etc/symbols	Fri Aug 03 19:08:15 2012 +0200
@@ -70,7 +70,7 @@
 \<FF>                   code: 0x01d509
 \<GG>                   code: 0x01d50a
 \<HH>                   code: 0x00210c
-#\<II>                   code: 0x01d50c
+\<II>                   code: 0x002111
 \<JJ>                   code: 0x01d50d
 \<KK>                   code: 0x01d50e
 \<LL>                   code: 0x01d50f
@@ -79,7 +79,7 @@
 \<OO>                   code: 0x01d512
 \<PP>                   code: 0x01d513
 \<QQ>                   code: 0x01d514
-#\<RR>                   code: 0x01d515
+\<RR>                   code: 0x00211c
 \<SS>                   code: 0x01d516
 \<TT>                   code: 0x01d517
 \<UU>                   code: 0x01d518
@@ -312,8 +312,6 @@
 \<emptyset>             code: 0x002205
 \<nabla>                code: 0x002207
 \<partial>              code: 0x002202
-\<Re>                   code: 0x00211c
-\<Im>                   code: 0x002111
 \<flat>                 code: 0x00266d
 \<natural>              code: 0x00266e
 \<sharp>                code: 0x00266f

--- a/src/Pure/Thy/html.ML	Fri Aug 03 17:56:35 2012 +0200
+++ b/src/Pure/Thy/html.ML	Fri Aug 03 19:08:15 2012 +0200
@@ -145,8 +145,6 @@
     ("\\<omega>", (1, "&omega;")),
     ("\\<bullet>", (1, "&bull;")),
     ("\\<dots>", (1, "&hellip;")),
-    ("\\<Re>", (1, "&real;")),
-    ("\\<Im>", (1, "&image;")),
     ("\\<wp>", (1, "&weierp;")),
     ("\\<forall>", (1, "&forall;")),
     ("\\<partial>", (1, "&part;")),

--- a/src/Tools/WWW_Find/www/find_theorems.js	Fri Aug 03 17:56:35 2012 +0200
+++ b/src/Tools/WWW_Find/www/find_theorems.js	Fri Aug 03 19:08:15 2012 +0200
@@ -24,7 +24,7 @@
 utf8['\\<preceq>'] = '≼';
 utf8['\\<nabla>'] = '∇';
 utf8['\\<FF>'] = '𝔉';
-utf8['\\<Im>'] = 'ℑ';
+utf8['\\<II>'] = 'ℑ';
 utf8['\\<VV>'] = '𝔙';
 utf8['\\<spacespace>'] = '␣';
 utf8['\\<and>'] = '∧';
@@ -141,7 +141,7 @@
 utf8['\\<QQ>'] = '𝔔';
 utf8['\\<setminus>'] = '∖';
 utf8['\\<Lambda>'] = 'Λ';
-utf8['\\<Re>'] = 'ℜ';
+utf8['\\<RR>'] = 'ℜ';
 utf8['\\<J>'] = '𝒥';
 utf8['\\<gg>'] = '𝔤';
 utf8['\\<hyphen>'] = '­';