# HG changeset patch
# User oheimb
# Date 981057381 -3600
# Node ID 17e9f0ba15ee141ec9765b9e37d4734abecc59aa
# Parent  a50365d21144ff4f9baef25ca5be5c2edda9bde7
added translations for bind_thm and val

diff -r a50365d21144 -r 17e9f0ba15ee lib/scripts/convert.pl
--- a/lib/scripts/convert.pl	Thu Feb 01 20:53:13 2001 +0100
+++ b/lib/scripts/convert.pl	Thu Feb 01 20:56:21 2001 +0100
@@ -28,6 +28,13 @@
   s/([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2\]/g;
 }
 
+sub subst_RS_fun {
+  my $s = shift;
+  $_ = $s;
+  subst_RS();
+  $_;
+}
+
 sub decl {
   my $s = shift;
   my $a = shift;
@@ -229,10 +236,12 @@
   s/^Goalw *(\[[\w\'\.\s,]*\]|[\w\'\. \[,\]]+) *(.+)/
     "lemma ".thmname().": $2$head"."apply (unfold ".thmlist($1).")"/se;
   s/^Goal *(.+)/"lemma ".thmname().": $1"/se;
-  s/ goal/"(*".thmname()."*) goal"/se; # ugly old-style goals
+  s/( |^)goal/"(*".thmname()."*)$1goal"/se; # ugly old-style goals
   s/^qed_spec_mp *\"(.*?)\"/done($1," [rule_format (no_asm)]")/se;
   s/^qed *\"(.*?)\"/done($1,"")/se;
   s/^bind_thm *\( *\"(.*?)\" *, *(.*?result *\( *\).*?) *\) *$/done($1,"[?? $2 ??] ")/se;
+  s/^bind_thm *\( *\"(.*?)\" *, *(.*?) *\) *$/"lemmas $1 = ".subst_RS_fun($2)/se;
+  s/^val *\( *\"(.*?)\" *= *(.*?) *\) *$/"lemmas $1 = ".subst_RS_fun($2)/se;
   s/^by(\s*\(?\s*)(.*?)\s*(\)?)\s*$/"apply$1".process_tac($1,$2).$3/se;
   s/^(apply +)\( *([\w\'\.]+)\s*\)\s*$/$1$2/;
                              # remove outermost parentheses if around atoms