# HG changeset patch
# User oheimb
# Date 988038679 -7200
# Node ID e502756bcb1129362eb8fbac1b2f97db1fb1c473
# Parent  9fde0021e1af363838e77bd2521284ea835e0ca8
added parentheses for 'b y' syntax, added primitive smp_tac support

diff -r 9fde0021e1af -r e502756bcb11 lib/scripts/convert.pl
--- 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;