# HG changeset patch
# User wenzelm
# Date 1375976947 -7200
# Node ID 0ea2b657eb420f4dda90cf38a77f6aec421942d1
# Parent  4539e4a0633964d5f0d11071f70dd20a262962c5
eliminate \<twosuperior> as well;

diff -r 4539e4a06339 -r 0ea2b657eb42 lib/Tools/update_sub_sup
--- a/lib/Tools/update_sub_sup	Thu Aug 08 17:36:14 2013 +0200
+++ b/lib/Tools/update_sub_sup	Thu Aug 08 17:49:07 2013 +0200
@@ -2,7 +2,7 @@
 #
 # Author: Makarius
 #
-# DESCRIPTION: update sub/sup control symbols
+# DESCRIPTION: update Isabelle symbols involving sub/superscripts
 
 
 ## diagnostics
@@ -14,7 +14,7 @@
   echo
   echo "Usage: isabelle $PRG [FILES|DIRS...]"
   echo
-  echo "  Recursively find .thy/.ML files and update control symbols for"
+  echo "  Recursively find .thy/.ML files and update Isabelle symbols involving"
   echo "  sub- and superscript."
   echo
   echo "  Old versions of files are preserved by appending \"~~\"."
diff -r 4539e4a06339 -r 0ea2b657eb42 lib/scripts/update_sub_sup
--- a/lib/scripts/update_sub_sup	Thu Aug 08 17:36:14 2013 +0200
+++ b/lib/scripts/update_sub_sup	Thu Aug 08 17:49:07 2013 +0200
@@ -2,7 +2,7 @@
 #
 # Author: Makarius
 #
-# update_sub_sup - update sub/sup control symbols
+# update_sub_sup - update Isabelle symbols involving sub/superscripts
 
 use warnings;
 use strict;
@@ -18,6 +18,9 @@
 
     s/\Q\<^isub>\E/\\<^sub>/g;
     s/\Q\<^isup>\E/\\<^sup>/g;
+    s/\Q\<onesuperior>\E/\\<^sup>1/g;
+    s/\Q\<twosuperior>\E/\\<^sup>2/g;
+    s/\Q\<threesuperior>\E/\\<^sup>3/g;
 
     my $result = $_;