added translations for bind_thm and val
authoroheimb
Thu Feb 01 20:56:21 2001 +0100 (2001-02-01)
changeset 1102717e9f0ba15ee
parent 11026 a50365d21144
child 11028 8cf44cbe22e8
added translations for bind_thm and val
lib/scripts/convert.pl
     1.1 --- a/lib/scripts/convert.pl	Thu Feb 01 20:53:13 2001 +0100
     1.2 +++ b/lib/scripts/convert.pl	Thu Feb 01 20:56:21 2001 +0100
     1.3 @@ -28,6 +28,13 @@
     1.4    s/([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2\]/g;
     1.5  }
     1.6  
     1.7 +sub subst_RS_fun {
     1.8 +  my $s = shift;
     1.9 +  $_ = $s;
    1.10 +  subst_RS();
    1.11 +  $_;
    1.12 +}
    1.13 +
    1.14  sub decl {
    1.15    my $s = shift;
    1.16    my $a = shift;
    1.17 @@ -229,10 +236,12 @@
    1.18    s/^Goalw *(\[[\w\'\.\s,]*\]|[\w\'\. \[,\]]+) *(.+)/
    1.19      "lemma ".thmname().": $2$head"."apply (unfold ".thmlist($1).")"/se;
    1.20    s/^Goal *(.+)/"lemma ".thmname().": $1"/se;
    1.21 -  s/ goal/"(*".thmname()."*) goal"/se; # ugly old-style goals
    1.22 +  s/( |^)goal/"(*".thmname()."*)$1goal"/se; # ugly old-style goals
    1.23    s/^qed_spec_mp *\"(.*?)\"/done($1," [rule_format (no_asm)]")/se;
    1.24    s/^qed *\"(.*?)\"/done($1,"")/se;
    1.25    s/^bind_thm *\( *\"(.*?)\" *, *(.*?result *\( *\).*?) *\) *$/done($1,"[?? $2 ??] ")/se;
    1.26 +  s/^bind_thm *\( *\"(.*?)\" *, *(.*?) *\) *$/"lemmas $1 = ".subst_RS_fun($2)/se;
    1.27 +  s/^val *\( *\"(.*?)\" *= *(.*?) *\) *$/"lemmas $1 = ".subst_RS_fun($2)/se;
    1.28    s/^by(\s*\(?\s*)(.*?)\s*(\)?)\s*$/"apply$1".process_tac($1,$2).$3/se;
    1.29    s/^(apply +)\( *([\w\'\.]+)\s*\)\s*$/$1$2/;
    1.30                               # remove outermost parentheses if around atoms