discontinued rendering of obsolete \<onesuperior>, \<twosuperior>, \<threesuperior>;
--- 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, "¯")),
("\\<degree>", (1, "°")),
("\\<plusminus>", (1, "±")),
- ("\\<twosuperior>", (1, "²")),
- ("\\<threesuperior>", (1, "³")),
("\\<acute>", (1, "´")),
("\\<paragraph>", (1, "¶")),
("\\<cdot>", (1, "·")),
("\\<cedilla>", (1, "¸")),
- ("\\<onesuperior>", (1, "¹")),
("\\<ordmasculine>", (1, "º")),
("\\<guillemotright>", (1, "»")),
("\\<onequarter>", (1, "¼")),
--- 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>'] = 'โ
';