test/Tools/isac/Knowledge/polyminus.sml
changeset 59823 4d222d137bb2
parent 59773 d88bb023c380
child 59852 ea7e6679080e
     1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Sat Mar 07 15:37:37 2020 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Sat Mar 07 17:11:55 2020 +0100
     1.3 @@ -416,7 +416,7 @@
     1.4  val ((pt,p),_) = get_calc 1; show_pt pt;
     1.5  "----- 1 ^^^";
     1.6  fetchApplicableTactics 1 0 p;
     1.7 -val appltacs = sel_appl_atomic_tacs pt p;
     1.8 +val appltacs = specific_from_prog pt p;
     1.9  applyTactic 1 p (hd appltacs) (*addiere_x_plus_minus*);
    1.10  val ((pt,p),_) = get_calc 1; show_pt pt;
    1.11  "----- 2 ^^^";
    1.12 @@ -438,21 +438,21 @@
    1.13  trace_rewrite := false;
    1.14  
    1.15  
    1.16 -applyTactic 1 p (hd (sel_appl_atomic_tacs pt p)) (*tausche_minus*);
    1.17 +applyTactic 1 p (hd (specific_from_prog pt p)) (*tausche_minus*);
    1.18  val ((pt,p),_) = get_calc 1; show_pt pt;
    1.19  "----- 3 ^^^";
    1.20 -applyTactic 1 p (hd (sel_appl_atomic_tacs pt p)) (**);
    1.21 +applyTactic 1 p (hd (specific_from_prog pt p)) (**);
    1.22  val ((pt,p),_) = get_calc 1; show_pt pt;
    1.23  "----- 4 ^^^";
    1.24 -applyTactic 1 p (hd (sel_appl_atomic_tacs pt p)) (**);
    1.25 +applyTactic 1 p (hd (specific_from_prog pt p)) (**);
    1.26  val ((pt,p),_) = get_calc 1; show_pt pt;
    1.27  "----- 5 ^^^";
    1.28 -applyTactic 1 p (hd (sel_appl_atomic_tacs pt p)) (**);
    1.29 +applyTactic 1 p (hd (specific_from_prog pt p)) (**);
    1.30  val ((pt,p),_) = get_calc 1; show_pt pt;
    1.31  "----- 6 ^^^";
    1.32  
    1.33  (*<CALCMESSAGE> failure </CALCMESSAGE>
    1.34 -applyTactic 1 p (hd (sel_appl_atomic_tacs pt p)) (**);
    1.35 +applyTactic 1 p (hd (specific_from_prog pt p)) (**);
    1.36  val ((pt,p),_) = get_calc 1; show_pt pt;
    1.37  "----- 7 ^^^";
    1.38  *)