removed (obsolete) mult_assumption
authoroheimb
Tue Jan 30 18:47:00 2001 +0100 (2001-01-30)
changeset 11000498d0db8cd8a
parent 10999 b044cf3500a2
child 11001 6754fa0f2af7
removed (obsolete) mult_assumption
lib/scripts/convert.pl
     1.1 --- a/lib/scripts/convert.pl	Tue Jan 30 14:48:27 2001 +0100
     1.2 +++ b/lib/scripts/convert.pl	Tue Jan 30 18:47:00 2001 +0100
     1.3 @@ -17,13 +17,6 @@
     1.4    $s;
     1.5  }
     1.6  
     1.7 -sub mult_assumption {
     1.8 -  my $n = shift;
     1.9 -  my $r = "";
    1.10 -  for($i=0; $i<$n; $i++) { $r = $r.", assumption"; }
    1.11 -  $r;
    1.12 -}
    1.13 -
    1.14  sub process_tac {
    1.15    my $lead = shift;
    1.16    my $t = shift;
    1.17 @@ -100,20 +93,19 @@
    1.18    s/rtac ([\w\.]+) 1/rule $1/g;
    1.19    s/rtac ([\w\.]+) (\d+)/rule_tac [$2] $1/g;
    1.20    s/res_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\.]+) 1/rule_tac $1 = $2 $3/g;
    1.21 -  s/ratac ([\w\.]+) (\d+) 1/"rule $1".mult_assumption($2)/eg;
    1.22    s/dtac ([\w\.]+) 1/drule $1/g;
    1.23    s/dtac ([\w\.]+) (\d+)/drule_tac [$2] $1/g;
    1.24    s/dres_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\.]+) 1/drule_tac $1 = $2 $3/g;
    1.25 -  s/datac ([\w\.]+) (\d+) 1/"drule $1".mult_assumption($2)/eg;
    1.26 +  s/datac ([\w\.]+) (\d+) 1/"drule ($2) $1"/g;
    1.27    s/etac ([\w\.]+) 1/erule $1/g;
    1.28    s/etac ([\w\.]+) (\d+)/erule_tac [$2] $1/g;
    1.29    s/eres_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\.]+) 1/erule_tac $1 = $2 $3/g;
    1.30 -  s/eatac ([\w\.]+) (\d+) 1/"erule $1".mult_assumption($2)/eg;
    1.31 +  s/eatac ([\w\.]+) (\d+) 1/"erule ($2) $1"/g;
    1.32    s/forward_tac \[([\w\.]+)\] 1/frule $1/g;
    1.33    s/ftac ([\w\.]+) 1/frule $1/g;
    1.34    s/ftac ([\w\.]+) (\d+)/frule_tac [$2] $1/g;
    1.35    s/forw_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\.]+) 1/frule_tac $1 = $2 $3/g;
    1.36 -  s/fatac ([\w\.]+) (\d+) 1/"frule $1".mult_assumption($2)/eg;
    1.37 +  s/fatac ([\w\.]+) (\d+) 1/"frule ($2) $1"/g;
    1.38  
    1.39  
    1.40    s/THEN /, /g;