prefer calligrapic \<RR> \<II> over \<Re> \<Im> for "screen" display (NB: official unicode defines only one version of these glyphs, unlike TeX);
authorwenzelm
Fri Aug 03 19:08:15 2012 +0200 (2012-08-03)
changeset 48670206144b13849
parent 48669 cdcdb0547f29
child 48671 951bc4c3ee17
prefer calligrapic \<RR> \<II> over \<Re> \<Im> for "screen" display (NB: official unicode defines only one version of these glyphs, unlike TeX);
etc/symbols
src/Pure/Thy/html.ML
src/Tools/WWW_Find/www/find_theorems.js
     1.1 --- a/etc/symbols	Fri Aug 03 17:56:35 2012 +0200
     1.2 +++ b/etc/symbols	Fri Aug 03 19:08:15 2012 +0200
     1.3 @@ -70,7 +70,7 @@
     1.4  \<FF>                   code: 0x01d509
     1.5  \<GG>                   code: 0x01d50a
     1.6  \<HH>                   code: 0x00210c
     1.7 -#\<II>                   code: 0x01d50c
     1.8 +\<II>                   code: 0x002111
     1.9  \<JJ>                   code: 0x01d50d
    1.10  \<KK>                   code: 0x01d50e
    1.11  \<LL>                   code: 0x01d50f
    1.12 @@ -79,7 +79,7 @@
    1.13  \<OO>                   code: 0x01d512
    1.14  \<PP>                   code: 0x01d513
    1.15  \<QQ>                   code: 0x01d514
    1.16 -#\<RR>                   code: 0x01d515
    1.17 +\<RR>                   code: 0x00211c
    1.18  \<SS>                   code: 0x01d516
    1.19  \<TT>                   code: 0x01d517
    1.20  \<UU>                   code: 0x01d518
    1.21 @@ -312,8 +312,6 @@
    1.22  \<emptyset>             code: 0x002205
    1.23  \<nabla>                code: 0x002207
    1.24  \<partial>              code: 0x002202
    1.25 -\<Re>                   code: 0x00211c
    1.26 -\<Im>                   code: 0x002111
    1.27  \<flat>                 code: 0x00266d
    1.28  \<natural>              code: 0x00266e
    1.29  \<sharp>                code: 0x00266f
     2.1 --- a/src/Pure/Thy/html.ML	Fri Aug 03 17:56:35 2012 +0200
     2.2 +++ b/src/Pure/Thy/html.ML	Fri Aug 03 19:08:15 2012 +0200
     2.3 @@ -145,8 +145,6 @@
     2.4      ("\\<omega>", (1, "&omega;")),
     2.5      ("\\<bullet>", (1, "&bull;")),
     2.6      ("\\<dots>", (1, "&hellip;")),
     2.7 -    ("\\<Re>", (1, "&real;")),
     2.8 -    ("\\<Im>", (1, "&image;")),
     2.9      ("\\<wp>", (1, "&weierp;")),
    2.10      ("\\<forall>", (1, "&forall;")),
    2.11      ("\\<partial>", (1, "&part;")),
     3.1 --- a/src/Tools/WWW_Find/www/find_theorems.js	Fri Aug 03 17:56:35 2012 +0200
     3.2 +++ b/src/Tools/WWW_Find/www/find_theorems.js	Fri Aug 03 19:08:15 2012 +0200
     3.3 @@ -24,7 +24,7 @@
     3.4  utf8['\\<preceq>'] = '≼';
     3.5  utf8['\\<nabla>'] = '∇';
     3.6  utf8['\\<FF>'] = '𝔉';
     3.7 -utf8['\\<Im>'] = 'ℑ';
     3.8 +utf8['\\<II>'] = 'ℑ';
     3.9  utf8['\\<VV>'] = '𝔙';
    3.10  utf8['\\<spacespace>'] = '␣';
    3.11  utf8['\\<and>'] = '∧';
    3.12 @@ -141,7 +141,7 @@
    3.13  utf8['\\<QQ>'] = '𝔔';
    3.14  utf8['\\<setminus>'] = '∖';
    3.15  utf8['\\<Lambda>'] = 'Λ';
    3.16 -utf8['\\<Re>'] = 'ℜ';
    3.17 +utf8['\\<RR>'] = 'ℜ';
    3.18  utf8['\\<J>'] = '𝒥';
    3.19  utf8['\\<gg>'] = '𝔤';
    3.20  utf8['\\<hyphen>'] = '­';