eliminate \<twosuperior> as well;
authorwenzelm
Thu Aug 08 17:49:07 2013 +0200 (2013-08-08)
changeset 529210ea2b657eb42
parent 52920 4539e4a06339
child 52922 d1bcb4479a2f
eliminate \<twosuperior> as well;
lib/Tools/update_sub_sup
lib/scripts/update_sub_sup
     1.1 --- a/lib/Tools/update_sub_sup	Thu Aug 08 17:36:14 2013 +0200
     1.2 +++ b/lib/Tools/update_sub_sup	Thu Aug 08 17:49:07 2013 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4  #
     1.5  # Author: Makarius
     1.6  #
     1.7 -# DESCRIPTION: update sub/sup control symbols
     1.8 +# DESCRIPTION: update Isabelle symbols involving sub/superscripts
     1.9  
    1.10  
    1.11  ## diagnostics
    1.12 @@ -14,7 +14,7 @@
    1.13    echo
    1.14    echo "Usage: isabelle $PRG [FILES|DIRS...]"
    1.15    echo
    1.16 -  echo "  Recursively find .thy/.ML files and update control symbols for"
    1.17 +  echo "  Recursively find .thy/.ML files and update Isabelle symbols involving"
    1.18    echo "  sub- and superscript."
    1.19    echo
    1.20    echo "  Old versions of files are preserved by appending \"~~\"."
     2.1 --- a/lib/scripts/update_sub_sup	Thu Aug 08 17:36:14 2013 +0200
     2.2 +++ b/lib/scripts/update_sub_sup	Thu Aug 08 17:49:07 2013 +0200
     2.3 @@ -2,7 +2,7 @@
     2.4  #
     2.5  # Author: Makarius
     2.6  #
     2.7 -# update_sub_sup - update sub/sup control symbols
     2.8 +# update_sub_sup - update Isabelle symbols involving sub/superscripts
     2.9  
    2.10  use warnings;
    2.11  use strict;
    2.12 @@ -18,6 +18,9 @@
    2.13  
    2.14      s/\Q\<^isub>\E/\\<^sub>/g;
    2.15      s/\Q\<^isup>\E/\\<^sup>/g;
    2.16 +    s/\Q\<onesuperior>\E/\\<^sup>1/g;
    2.17 +    s/\Q\<twosuperior>\E/\\<^sup>2/g;
    2.18 +    s/\Q\<threesuperior>\E/\\<^sup>3/g;
    2.19  
    2.20      my $result = $_;
    2.21