--- a/lib/scripts/convert.pl Fri Apr 20 17:18:47 2001 +0200
+++ b/lib/scripts/convert.pl Mon Apr 23 17:11:19 2001 +0200
@@ -119,6 +119,7 @@
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;
@@ -257,7 +258,7 @@
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;