lib/scripts/convert.pl

 #
 # convert.pl - convert legacy tactic scripts to Isabelle/Isar tactic
 #   emulation using heuristics - leaves unrecognized patterns unchanged
 #   produces from each input file (on the command line) a new file with
 #   ".thy" appended and renames the original input file by appending "~0~"
-
 
 sub thmlist {
   my $s = shift;
   $s =~ s/^\[(.*)\]$/$1/sg;
   $s =~ s/, +/ /g;

     $finalfile = "$currfile.thy";
     $tmpfile   = "$finalfile.~0~";
     open(ARGVOUT, '>'.$tmpfile);
     select(ARGVOUT);
   }
-
  nl:
   if(!s/;(\s*?(\n?$|\(\*))/$1/s && !eof()) {# no end_of_ML_command marker
     $_ = $_ . <>;
     goto nl;
   }
   s/\\(\s*\n\s*)\\/ $1 /g; # remove backslashes escaping newlines
  nlc:
   m/^(\s*)(.*?)(\s*)$/s;
   $head=$1; $line=$2; $tail=$3;
   $tail =~ s/\s+\n/\n/sg;  # remove trailing whitespace at end of lines
+  $line =~ s/\\\\<(\^?)(\w+)>/\\<$1$2>/g; # convert \\<...> to \<...> and \\<^...> to \<^...>
   print $head; $_=$line.$tail;
   if ($line =~ m/^\(\*/) { # start comment
     while (($i = index $_,"*)") == -1 && !eof()) { # no end comment
+      s/\\\\<(\^?)(\w+)>/\\<$1$2>/g; # convert \\<...> to \<...> and \\<^...> to \<^...>
       print;
       $_ = <>;
     }
     if ($i == -1) { print; last; } 
     print substr $_,0,$i+2;