lib/scripts/convert.pl

   s/hypsubst_tac 1/hypsubst/g;
   s/arith_tac 1/arith/g;
   s/strip_tac 1/intro strip/g;
   s/split_all_tac 1/simp (no_asm_simp) only: split_tupled_all/g;
 
+  s/smp_tac (\d+) (\d+)/tactic "smp_tac $1 $2"/g;
   s/rotate_tac (\d+) (\d+)/rotate_tac [$2] $1/g;
   s/rotate_tac ~ *(\d+) (\d+)/rotate_tac [$2] -$1/g;
   s/rename_tac (\".*?\") (\d+)/rename_tac [$2] $1/g;
   s/case_tac (\".*?\") (\d+)/case_tac [$2] $1/g;
   s/induct_tac (\".*?\") (\d+)/induct_tac [$2] $1/g;

   s/^val *(\w+) *= *result *\( *\) *$/done($1,"")/se;
   s/^bind_thm *\( *\"(.*?)\" *, *(result *\( *\) *?) *\) *$/done($1,"")/se;
   s/^bind_thm *\( *\"(.*?)\" *, *(.*?result *\( *\).*?) *\) *$/done($1,"[?? $2 ??] ")/se;
   s/^bind_thm *\( *\"(.*?)\" *, *(.*?) *\) *$/"lemmas $1 = ".subst_RS_standard($2)/se;
   s/^by(\s*\(?\s*)(.*?)\s*(\)?)\s*$/process_tac($1,$2).$3/se;
-  s/^b\sy(\s*)(.*?)(\s*)$/process_tac($1,$2).$3/se;
+  s/^b\s+y(\s*)(.*?)(\s*)$/process_tac($1,"(".$2.")").$3/se;
   s/^(apply +)\( *([\w\'\.]+)\s*\)\s*$/$1$2/;
                              # remove outermost parentheses if around atoms
   s/^Addsimps\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"simp")/seg;
   s/^Delsimps\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"simp del")/seg;
   s/^Addsplits\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"split")/seg;