# HG changeset patch
# User streckem
# Date 983981956 -3600
# Node ID 26a3e549ce8ed55d5917b677cf9e1523ef3c3340
# Parent  4b365574c7c4f74ce25a3b98cb6c58e1e49bf85f
added strange 'b y' syntax

diff -r 4b365574c7c4 -r 26a3e549ce8e lib/scripts/convert.pl
--- a/lib/scripts/convert.pl	Wed Mar 07 16:25:51 2001 +0100
+++ b/lib/scripts/convert.pl	Wed Mar 07 17:19:16 2001 +0100
@@ -257,6 +257,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/^(apply +)\( *([\w\'\.]+)\s*\)\s*$/$1$2/;
                              # remove outermost parentheses if around atoms
   s/^Addsimps\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"simp")/seg;