# HG changeset patch
# User wenzelm
# Date 1377457029 -7200
# Node ID 1943db7bc34c14fb9a2783f35e7d4f5752cd3eb8
# Parent  2ddc5e788f7c4478f8b5700574c949eea4003936
discontinued rendering of obsolete \<onesuperior>, \<twosuperior>, \<threesuperior>;

diff -r 2ddc5e788f7c -r 1943db7bc34c etc/symbols
--- 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
diff -r 2ddc5e788f7c -r 1943db7bc34c lib/texinputs/isabellesym.sty
--- 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
diff -r 2ddc5e788f7c -r 1943db7bc34c src/Pure/Thy/html.ML
--- 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;")),
diff -r 2ddc5e788f7c -r 1943db7bc34c src/Tools/WWW_Find/www/find_theorems.js
--- 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>'] = '⋅';