discontinued rendering of obsolete \<onesuperior>, \<twosuperior>, \<threesuperior>;
authorwenzelm
Sun, 25 Aug 2013 20:57:09 +0200
changeset 53194 1943db7bc34c
parent 53193 2ddc5e788f7c
child 53195 e4b18828a817
discontinued rendering of obsolete \<onesuperior>, \<twosuperior>, \<threesuperior>;
etc/symbols
lib/texinputs/isabellesym.sty
src/Pure/Thy/html.ML
src/Tools/WWW_Find/www/find_theorems.js
--- a/etc/symbols	Sun Aug 25 20:43:10 2013 +0200
+++ b/etc/symbols	Sun Aug 25 20:57:09 2013 +0200
@@ -320,11 +320,8 @@
 \<registered>           code: 0x0000ae
 \<hyphen>               code: 0x0000ad  group: punctuation
 \<inverse>              code: 0x0000af  group: punctuation
-\<onesuperior>          code: 0x0000b9  group: digit
 \<onequarter>           code: 0x0000bc  group: digit
-\<twosuperior>          code: 0x0000b2  group: digit
 \<onehalf>              code: 0x0000bd  group: digit
-\<threesuperior>        code: 0x0000b3  group: digit
 \<threequarters>        code: 0x0000be  group: digit
 \<ordfeminine>          code: 0x0000aa
 \<ordmasculine>         code: 0x0000ba
--- a/lib/texinputs/isabellesym.sty	Sun Aug 25 20:43:10 2013 +0200
+++ b/lib/texinputs/isabellesym.sty	Sun Aug 25 20:57:09 2013 +0200
@@ -322,13 +322,9 @@
 \newcommand{\isasymangle}{\isamath{\angle}}
 \newcommand{\isasymcopyright}{\isatext{\rm\copyright}}
 \newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
-\newcommand{\isasymhyphen}{\isatext{\rm-}}
 \newcommand{\isasyminverse}{\isamath{{}^{-1}}}
-\newcommand{\isasymonesuperior}{\isamath{{}^1}}
 \newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}}  %requires textcomp
-\newcommand{\isasymtwosuperior}{\isamath{{}^2}}
 \newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}}  %requires textcomp
-\newcommand{\isasymthreesuperior}{\isamath{{}^3}}
 \newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}}  %requires textcomp
 \newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
 \newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
@@ -342,6 +338,7 @@
 \newcommand{\isasymcent}{\isatext{\textcent}}  %requires textcomp
 \newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
 \newcommand{\isasymdegree}{\isatext{\rm\textdegree}}  %requires textcomp
+\newcommand{\isasymhyphen}{\isatext{\rm-}}
 \newcommand{\isasymamalg}{\isamath{\amalg}}
 \newcommand{\isasymmho}{\isamath{\mho}}  %requires amssymb
 \newcommand{\isasymlozenge}{\isamath{\lozenge}}  %requires amssymb
--- a/src/Pure/Thy/html.ML	Sun Aug 25 20:43:10 2013 +0200
+++ b/src/Pure/Thy/html.ML	Sun Aug 25 20:57:09 2013 +0200
@@ -77,13 +77,10 @@
     ("\\<inverse>", (1, "&macr;")),
     ("\\<degree>", (1, "&deg;")),
     ("\\<plusminus>", (1, "&plusmn;")),
-    ("\\<twosuperior>", (1, "&sup2;")),
-    ("\\<threesuperior>", (1, "&sup3;")),
     ("\\<acute>", (1, "&acute;")),
     ("\\<paragraph>", (1, "&para;")),
     ("\\<cdot>", (1, "&middot;")),
     ("\\<cedilla>", (1, "&cedil;")),
-    ("\\<onesuperior>", (1, "&sup1;")),
     ("\\<ordmasculine>", (1, "&ordm;")),
     ("\\<guillemotright>", (1, "&raquo;")),
     ("\\<onequarter>", (1, "&frac14;")),
--- a/src/Tools/WWW_Find/www/find_theorems.js	Sun Aug 25 20:43:10 2013 +0200
+++ b/src/Tools/WWW_Find/www/find_theorems.js	Sun Aug 25 20:57:09 2013 +0200
@@ -167,7 +167,6 @@
 utf8['\\<mho>'] = 'โ„ง';
 utf8['\\<O>'] = '๐’ช';
 utf8['\\<rr>'] = '๐”ฏ';
-utf8['\\<twosuperior>'] = 'ยฒ';
 utf8['\\<leftharpoonup>'] = 'โ†ผ';
 utf8['\\<pi>'] = 'ฯ€';
 utf8['\\<k>'] = '๐—„';
@@ -188,7 +187,6 @@
 utf8['\\<ii>'] = '๐”ฆ';
 utf8['\\<hookleftarrow>'] = 'โ†ฉ';
 utf8['\\<P>'] = '๐’ซ';
-utf8['\\<threesuperior>'] = 'ยณ';
 utf8['\\<epsilon>'] = 'ฮต';
 utf8['\\<yy>'] = '๐”ถ';
 utf8['\\<h>'] = '๐—';
@@ -231,7 +229,6 @@
 utf8['\\<V>'] = '๐’ฑ';
 utf8['\\<ss>'] = '๐”ฐ';
 utf8['\\<unrhd>'] = 'โŠต';
-utf8['\\<onesuperior>'] = 'ยน';
 utf8['\\<b>'] = '๐–ป';
 utf8['\\<downharpoonleft>'] = 'โ‡ƒ';
 utf8['\\<cdot>'] = 'โ‹…';