diff -r 7f29665daeb2 -r 5eba5e6d5266 test/Tools/isac/Frontend/use-cases.sml
--- a/test/Tools/isac/Frontend/use-cases.sml	Wed Oct 05 10:51:25 2016 +0200
+++ b/test/Tools/isac/Frontend/use-cases.sml	Wed Oct 05 13:09:54 2016 +0200
@@ -110,30 +110,30 @@
 
  fetchProposedTactic 1 (*by using Iterator No.1*);
  setNextTactic 1 (Model_Problem); (*by using Iterator No.1*)
- autoCalculate' 1 (Step 1);
+ autoCalculate 1 (Step 1);
  refFormula 1 (get_pos 1 1)  (*model contains descriptions for all items*);
- autoCalculate' 1 (Step 1);
+ autoCalculate 1 (Step 1);
 (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
  fetchProposedTactic 1;
  setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)");
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);
 
  fetchProposedTactic 1;
  setNextTactic 1 (Add_Given "solveFor x");
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 
  fetchProposedTactic 1;
  setNextTactic 1 (Add_Find "solutions L");
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 
  fetchProposedTactic 1;
  setNextTactic 1 (Specify_Theory "Test");
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
 
  fetchProposedTactic 1;
  setNextTactic 1 (Specify_Problem ["LINEAR","univariate","equation","test"]);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 (*-------------------------------------------------------------------------*)
  fetchProposedTactic 1;
  val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
@@ -141,7 +141,7 @@
  setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
  val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
 
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
  val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
 
 (*-------------------------------------------------------------------------*)
@@ -154,22 +154,22 @@
  is_complete_mod ptp;
  is_complete_spec ptp;
 
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
  val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
  (*term2str (get_obj g_form pt [1]);*)
 (*-------------------------------------------------------------------------*)
 
  fetchProposedTactic 1;
  setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 
  fetchProposedTactic 1;
  setNextTactic 1 (Rewrite_Set "Test_simplify");
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 
  fetchProposedTactic 1;
  setNextTactic 1 (Check_Postcond ["LINEAR","univariate","equation","test"]);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 
  val ((pt,_),_) = get_calc 1;
  val ip = get_pos 1 1;
@@ -217,104 +217,104 @@
  refFormula 1 (get_pos 1 1);
  fetchProposedTactic 1;
  setNextTactic 1 (Model_Problem);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*gets ModSpec;model is still empty*)
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*gets ModSpec;model is still empty*)
 
  fetchProposedTactic 1;
  setNextTactic 1 (Add_Given "equality (x + 1 = 2)");
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 
  fetchProposedTactic 1;
  setNextTactic 1 (Add_Given "solveFor x");
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 
  fetchProposedTactic 1;
  setNextTactic 1 (Add_Find "solutions L");
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 
  fetchProposedTactic 1;
  setNextTactic 1 (Specify_Theory "Test");
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 
  fetchProposedTactic 1;
  setNextTactic 1 (Specify_Problem 
 		      ["sqroot-test","univariate","equation","test"]);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 "1-----------------------------------------------------------------";
 
  fetchProposedTactic 1;
  setNextTactic 1 (Specify_Method ["Test","squ-equ-test-subpbl1"]);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 
  fetchProposedTactic 1;
  setNextTactic 1 (Apply_Method ["Test","squ-equ-test-subpbl1"]);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 
  fetchProposedTactic 1;
  setNextTactic 1 (Rewrite_Set "norm_equation");
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 
  fetchProposedTactic 1;
  setNextTactic 1 (Rewrite_Set "Test_simplify");
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 
  fetchProposedTactic 1;(*----------------Subproblem--------------------*);
  setNextTactic 1 (Subproblem ("Test",
 			      ["LINEAR","univariate","equation","test"]));
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 
  fetchProposedTactic 1;
  setNextTactic 1 (Model_Problem );
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 
  fetchProposedTactic 1;
  setNextTactic 1 (Add_Given "equality (-1 + x = 0)");
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 
  fetchProposedTactic 1;
  setNextTactic 1 (Add_Given "solveFor x");
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 
  fetchProposedTactic 1;
  setNextTactic 1 (Add_Find "solutions x_i");
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 
  fetchProposedTactic 1;
  setNextTactic 1 (Specify_Theory "Test");
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 
  fetchProposedTactic 1;
  setNextTactic 1 (Specify_Problem ["LINEAR","univariate","equation","test"]);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 "2-----------------------------------------------------------------";
 
  fetchProposedTactic 1;
  setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 
  fetchProposedTactic 1;
  setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 
  fetchProposedTactic 1;
  setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 
  fetchProposedTactic 1;
  setNextTactic 1 (Rewrite_Set "Test_simplify");
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 
  fetchProposedTactic 1;
  setNextTactic 1 (Check_Postcond ["LINEAR","univariate","equation","test"]);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 
  fetchProposedTactic 1;
  setNextTactic 1 (Check_elementwise "Assumptions");
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 
  val xml = fetchProposedTactic 1;
  setNextTactic 1 (Check_Postcond 
 		      ["sqroot-test","univariate","equation","test"]);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 
  val ((pt,_),_) = get_calc 1;
  val str = pr_ptree pr_short pt;
@@ -335,39 +335,39 @@
     ["Test","squ-equ-test-subpbl1"]))];
  Iterator 1;
  moveActiveRoot 1;
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
  (*here the solve-phase starts*)
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
  (*------------------------------------*)
 (* default_print_depth 13; get_calc 1;
    *)
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
  (*calc-head of subproblem*)
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
  (*solve-phase of the subproblem*)
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
  (*finish subproblem*)
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
  (*finish problem*)
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1); 
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); 
 
  (*this checks the test for correctness..*)
  val ((pt,_),_) = get_calc 1;
@@ -391,7 +391,7 @@
  moveActiveRoot 1;
 getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 999 false;
 
- autoCalculate' 1 CompleteCalc; 
+ autoCalculate 1 CompleteCalc; 
  val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
  getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
 
@@ -414,11 +414,11 @@
  Iterator 1;
  moveActiveRoot 1;
 
- autoCalculate' 1 CompleteCalcHead;
+ autoCalculate 1 CompleteCalcHead;
  refFormula 1 (get_pos 1 1);
  val ((pt,p),_) = get_calc 1;
 
- autoCalculate' 1 CompleteCalc; 
+ autoCalculate 1 CompleteCalc; 
  val ((pt,p),_) = get_calc 1;
  if p=([], Res) then () else 
  error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Calc ";
@@ -433,7 +433,7 @@
     ["Test","squ-equ-test-subpbl1"]))];
  Iterator 1;
  moveActiveRoot 1;
- autoCalculate' 1 CompleteCalc;
+ autoCalculate 1 CompleteCalc;
  val ((pt,p),_) = get_calc 1; show_pt pt;
 (*
 getTactic 1 ([1],Frm);
@@ -461,7 +461,7 @@
     ["Test","squ-equ-test-subpbl1"]))];
  Iterator 1;
  moveActiveRoot 1;
- autoCalculate' 1 CompleteCalcHead;
+ autoCalculate 1 CompleteCalcHead;
 
 val ((Nd (PblObj {env = NONE, fmz = (fm, ("Test", pblID, metID)), loc = (SOME (env, ctxt1), NONE), 
       cell = NONE, ctxt = ctxt2, meth,
@@ -483,7 +483,7 @@
 	["Test","solve_linear"]))];
  Iterator 1;
  moveActiveRoot 1;
- autoCalculate' 1 CompleteModel;  
+ autoCalculate 1 CompleteModel;  
  refFormula 1 (get_pos 1 1);
 
 setProblem 1 ["LINEAR","univariate","equation","test"];
@@ -500,9 +500,9 @@
 			    ["Test","solve_linear"]) then ()
  else error "FE-interface.sml: diff.behav. in setProblem, setMethod";
 
- autoCalculate' 1 CompleteCalcHead;
+ autoCalculate 1 CompleteCalcHead;
  refFormula 1 (get_pos 1 1); 
- autoCalculate' 1 CompleteCalc; 
+ autoCalculate 1 CompleteCalc; 
  moveActiveDown 1;
  moveActiveDown 1;
  moveActiveDown 1;
@@ -522,31 +522,31 @@
   ("Test", ["sqroot-test","univariate","equation","test"],
    ["Test","squ-equ-test-subpbl1"]))];
  Iterator 1; moveActiveRoot 1;
- autoCalculate' 1 CompleteCalcHead;
- autoCalculate' 1 (Step 1);
+ autoCalculate 1 CompleteCalcHead;
+ autoCalculate 1 (Step 1);
  val ((pt,p),_) = get_calc 1;  show_pt pt; (*2 lines, OK*)
  (*
  setNextTactic 1 (Rewrite_Set "Test_simplify"); (*--> "thy_isac_Test-rls-Test_simplify"*)
- autoCalculate' 1 (Step 1);
+ autoCalculate 1 (Step 1);
  val ((pt,p),_) = get_calc 1;  show_pt pt;
  *)
 "-----^^^^^ and vvvvv do the same -----";
  setContext 1 p "thy_isac_Test-rls-Test_simplify";
  val ((pt,p),_) = get_calc 1;  show_pt pt; (*2 lines, OK*)
 
- autoCalculate' 1 (Step 1);
+ autoCalculate 1 (Step 1);
  setContext 1 p "thy_isac_Test-rls-Test_simplify";
  val (((pt,_),_), p) = (get_calc 1, get_pos 1 1);
  val (Form f, tac, asms) = pt_extract (pt, p);
  if p = ([1], Res) andalso term2str (get_obj g_res pt (fst p)) = "x + 1 + -1 * 2 = 0"
- then () else error "--- setContext..Thy --- autoCalculate' 1 (Step 1) #1";
+ then () else error "--- setContext..Thy --- autoCalculate 1 (Step 1) #1";
 
- autoCalculate' 1 CompleteCalc;
+ autoCalculate 1 CompleteCalc;
  val (((pt,_),_), p) = (get_calc 1, get_pos 1 1);
  val (Form f, tac, asms) = pt_extract (pt, p);
 
  if term2str f = "[x = 1]" andalso p = ([], Res) then () 
-  else error "--- setContext..Thy --- autoCalculate' CompleteCalc";
+  else error "--- setContext..Thy --- autoCalculate CompleteCalc";
  DEconstrCalcTree 1;
 
 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
@@ -556,7 +556,7 @@
    ("Test", ["sqroot-test","univariate","equation","test"],
     ["Test","squ-equ-test-subpbl1"]))];
  Iterator 1; moveActiveRoot 1;
- autoCalculate' 1 CompleteToSubpbl;
+ autoCalculate 1 CompleteToSubpbl;
  refFormula 1 (get_pos 1 1); (*<ISA> -1 + x = 0 </ISA>*);
  val ((pt,_),_) = get_calc 1;
  val str = pr_ptree pr_short pt;
@@ -565,12 +565,12 @@
  then () else 
  error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl-1";
 
- autoCalculate' 1 (Step 1); (*proceeds only, of NOT 1 step before subplb*)
- autoCalculate' 1 CompleteToSubpbl;
+ autoCalculate 1 (Step 1); (*proceeds only, of NOT 1 step before subplb*)
+ autoCalculate 1 CompleteToSubpbl;
  val ((pt,_),_) = get_calc 1;
  val str = pr_ptree pr_short pt;
  writeln str;
- autoCalculate' 1 CompleteCalc; (*das geht ohnehin !*);
+ autoCalculate 1 CompleteCalc; (*das geht ohnehin !*);
  val ((pt,_),_) = get_calc 1;
  val p = get_pos 1 1;
 
@@ -590,72 +590,72 @@
  fetchProposedTactic 1;
 
  setNextTactic 1 (Model_Problem);
- autoCalculate' 1 (Step 1); fetchProposedTactic 1;
+ autoCalculate 1 (Step 1); fetchProposedTactic 1;
 
  setNextTactic 1 (Specify_Theory "RatEq");
- autoCalculate' 1 (Step 1); fetchProposedTactic 1;
+ autoCalculate 1 (Step 1); fetchProposedTactic 1;
  setNextTactic 1 (Specify_Problem ["rational","univariate","equation"]);
- autoCalculate' 1 (Step 1); fetchProposedTactic 1;
+ autoCalculate 1 (Step 1); fetchProposedTactic 1;
  setNextTactic 1 (Specify_Method ["RatEq","solve_rat_equation"]);
- autoCalculate' 1 (Step 1); fetchProposedTactic 1;
+ autoCalculate 1 (Step 1); fetchProposedTactic 1;
  setNextTactic 1 (Apply_Method ["RatEq","solve_rat_equation"]);
- autoCalculate' 1 (Step 1); fetchProposedTactic 1;
+ autoCalculate 1 (Step 1); fetchProposedTactic 1;
  setNextTactic 1 (Rewrite_Set "RatEq_simplify");
- autoCalculate' 1 (Step 1); fetchProposedTactic 1;
+ autoCalculate 1 (Step 1); fetchProposedTactic 1;
  setNextTactic 1 (Rewrite_Set "norm_Rational");
- autoCalculate' 1 (Step 1); fetchProposedTactic 1;
+ autoCalculate 1 (Step 1); fetchProposedTactic 1;
  setNextTactic 1 (Rewrite_Set "RatEq_eliminate");
- autoCalculate' 1 (Step 1); fetchProposedTactic 1;
+ autoCalculate 1 (Step 1); fetchProposedTactic 1;
  (*               __________ for "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)"*)
  setNextTactic 1 (Subproblem ("PolyEq", ["normalize","polynomial",
 					    "univariate","equation"]));
- autoCalculate' 1 (Step 1); fetchProposedTactic 1;
+ autoCalculate 1 (Step 1); fetchProposedTactic 1;
  setNextTactic 1 (Model_Problem );
- autoCalculate' 1 (Step 1); fetchProposedTactic 1;
+ autoCalculate 1 (Step 1); fetchProposedTactic 1;
  setNextTactic 1 (Specify_Theory "PolyEq");
- autoCalculate' 1 (Step 1); fetchProposedTactic 1;
+ autoCalculate 1 (Step 1); fetchProposedTactic 1;
  setNextTactic 1 (Specify_Problem ["normalize","polynomial",
 				   "univariate","equation"]);
- autoCalculate' 1 (Step 1); fetchProposedTactic 1;
+ autoCalculate 1 (Step 1); fetchProposedTactic 1;
  setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
- autoCalculate' 1 (Step 1); fetchProposedTactic 1;
+ autoCalculate 1 (Step 1); fetchProposedTactic 1;
  setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
- autoCalculate' 1 (Step 1); fetchProposedTactic 1;
+ autoCalculate 1 (Step 1); fetchProposedTactic 1;
  setNextTactic 1 (Rewrite ("all_left",""));
- autoCalculate' 1 (Step 1); fetchProposedTactic 1;
+ autoCalculate 1 (Step 1); fetchProposedTactic 1;
  setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));
- autoCalculate' 1 (Step 1); fetchProposedTactic 1;
+ autoCalculate 1 (Step 1); fetchProposedTactic 1;
  (*               __________ for "16 + 12 * x = 0"*)
  setNextTactic 1 (Subproblem ("PolyEq",
 			 ["degree_1","polynomial","univariate","equation"]));
- autoCalculate' 1 (Step 1); fetchProposedTactic 1;
+ autoCalculate 1 (Step 1); fetchProposedTactic 1;
  setNextTactic 1 (Model_Problem );
- autoCalculate' 1 (Step 1); fetchProposedTactic 1;
+ autoCalculate 1 (Step 1); fetchProposedTactic 1;
  setNextTactic 1 (Specify_Theory "PolyEq");
  (*------------- some trials in the problem-hierarchy ---------------*)
  setNextTactic 1 (Specify_Problem ["LINEAR","univariate","equation"]);
- autoCalculate' 1 (Step 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
+ autoCalculate 1 (Step 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
  setNextTactic 1 (Refine_Problem ["univariate","equation"]);
  (*------------------------------------------------------------------*)
- autoCalculate' 1 (Step 1); fetchProposedTactic 1;
+ autoCalculate 1 (Step 1); fetchProposedTactic 1;
  setNextTactic 1 (Specify_Method ["PolyEq","solve_d1_polyeq_equation"]);
- autoCalculate' 1 (Step 1); fetchProposedTactic 1;
+ autoCalculate 1 (Step 1); fetchProposedTactic 1;
  setNextTactic 1 (Apply_Method ["PolyEq","solve_d1_polyeq_equation"]);
- autoCalculate' 1 (Step 1); fetchProposedTactic 1;
+ autoCalculate 1 (Step 1); fetchProposedTactic 1;
  setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "d1_polyeq_simplify"));
- autoCalculate' 1 (Step 1); fetchProposedTactic 1;
+ autoCalculate 1 (Step 1); fetchProposedTactic 1;
  setNextTactic 1 (Rewrite_Set "polyeq_simplify");
- autoCalculate' 1 (Step 1); fetchProposedTactic 1;
+ autoCalculate 1 (Step 1); fetchProposedTactic 1;
  setNextTactic 1 Or_to_List;
- autoCalculate' 1 (Step 1); fetchProposedTactic 1;
+ autoCalculate 1 (Step 1); fetchProposedTactic 1;
  setNextTactic 1 (Check_elementwise "Assumptions"); 
- autoCalculate' 1 (Step 1); fetchProposedTactic 1;
+ autoCalculate 1 (Step 1); fetchProposedTactic 1;
  setNextTactic 1 (Check_Postcond ["degree_1","polynomial",
 				  "univariate","equation"]);
- autoCalculate' 1 (Step 1); fetchProposedTactic 1;
+ autoCalculate 1 (Step 1); fetchProposedTactic 1;
  setNextTactic 1 (Check_Postcond ["normalize","polynomial",
 				  "univariate","equation"]);
- autoCalculate' 1 (Step 1); fetchProposedTactic 1;
+ autoCalculate 1 (Step 1); fetchProposedTactic 1;
  setNextTactic 1 (Check_Postcond ["rational","univariate","equation"]);
  val (ptp,_) = get_calc 1;
  val (Form t,_,_) = pt_extract ptp;
@@ -683,16 +683,16 @@
  (*..this tactic should be done 'tacitly', too !*)
 
 (*
-autoCalculate' 1 CompleteCalcHead; 
+autoCalculate 1 CompleteCalcHead; 
 checkContext 1 ([],Pbl) "pbl_equ_univ";
 checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
 *)
 
- autoCalculate' 1 (Step 1); 
+ autoCalculate 1 (Step 1); 
 
  fetchProposedTactic 1;
  setNextTactic 1 (Add_Given "equality (x ^^^ 2 + 4 * x + 5 = (2::real))");
- autoCalculate' 1 (Step 1); 
+ autoCalculate 1 (Step 1); 
 
  "--------- we go into the ProblemBrowser (_NO_ pblID selected) -";
 initContext 1 Pbl_ ([],Pbl);
@@ -711,10 +711,10 @@
 
 
  fetchProposedTactic 1;
- setNextTactic 1 (Add_Given "solveFor x"); autoCalculate' 1 (Step 1);
+ setNextTactic 1 (Add_Given "solveFor x"); autoCalculate 1 (Step 1);
 
  fetchProposedTactic 1;
- setNextTactic 1 (Add_Find "solutions L"); autoCalculate' 1 (Step 1);
+ setNextTactic 1 (Add_Find "solutions L"); autoCalculate 1 (Step 1);
 
  "--------- this is a matching model (all items correct): -------";
 checkContext 1  ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
@@ -732,25 +732,25 @@
  "--------- this is done by <TRANSFER> on the pbl-browser: ------";
  setNextTactic 1 (Specify_Problem ["normalize","polynomial",
 				 "univariate","equation"]);
- autoCalculate' 1 (Step 1);
+ autoCalculate 1 (Step 1);
 (*WN050904 fetchProposedTactic again --> Specify_Problem ["normalize",...
   and Specify_Theory skipped in comparison to below ---^^^-inserted      *)
 (*------------vvv-inserted-----------------------------------------------*)
  fetchProposedTactic 1;
  setNextTactic 1 (Specify_Problem ["normalize","polynomial",
 				 "univariate","equation"]);
- autoCalculate' 1 (Step 1);
+ autoCalculate 1 (Step 1);
 
 (*and Specify_Theory skipped by fetchProposedTactic ?!?*)
 
  fetchProposedTactic 1;
  setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
- autoCalculate' 1 (Step 1);
+ autoCalculate 1 (Step 1);
 
  fetchProposedTactic 1;
  setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
 
- autoCalculate' 1 CompleteCalc;
+ autoCalculate 1 CompleteCalc;
 
  val ((pt,_),_) = get_calc 1;
  show_pt pt;
@@ -764,15 +764,15 @@
   before, too, because there was no check*)
  fetchProposedTactic 1;
  setNextTactic 1 (Specify_Theory "PolyEq");
- autoCalculate' 1 (Step 1);
+ autoCalculate 1 (Step 1);
 
  fetchProposedTactic 1;
  setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
- autoCalculate' 1 (Step 1);
+ autoCalculate 1 (Step 1);
 
  fetchProposedTactic 1;
  "--------- now the calc-header is ready for enter 'solving' ----";
- autoCalculate' 1 CompleteCalc;
+ autoCalculate 1 CompleteCalc;
 
  val ((pt,_),_) = get_calc 1;
  rootthy pt;
@@ -882,7 +882,7 @@
  fetchProposedTactic 1;
 (*fill the CalcHead with Descriptions...*)
  setNextTactic 1 (Model_Problem );
- autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
 
  (*user input is !!!!!EITHER!!!!! _some_ (at least one) items of the model 
  !!!!!OR!!!!! _one_ part of the specification !!!!!!!!!!!!!*)
@@ -902,7 +902,7 @@
  fetchProposedTactic 1;
  (*the student follows the advice*)
  setNextTactic 1 (Add_Find "maximum A"); (*FIXME.17.11.03: does not yet work*)
-  autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
+  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
  
  (*this input completes the model*)
  modifyCalcHead 1 (([],Pbl), "not used here",
@@ -949,7 +949,7 @@
 		  Pbl, 
 		  ("Test", ["LINEAR","univariate","equation","test"],
 		   ["Test","solve_linear"]));
- autoCalculate' 1 CompleteCalc;
+ autoCalculate 1 CompleteCalc;
  refFormula 1 (get_pos 1 1);
  val ((pt,_),_) = get_calc 1;
  val p = get_pos 1 1;
@@ -967,7 +967,7 @@
  CalcTree [(fmz, sp)];
  Iterator 1; moveActiveRoot 1;
  modifyCalcHead 1 (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], []));
- autoCalculate' 1 CompleteCalc;
+ autoCalculate 1 CompleteCalc;
  refFormula 1 (get_pos 1 1);
  val ((pt,_),_) = get_calc 1;
  val p = get_pos 1 1;
@@ -985,7 +985,7 @@
     ["Test","squ-equ-test-subpbl1"]))];
  Iterator 1;
  moveActiveRoot 1;
- autoCalculate' 1 CompleteCalc; 
+ autoCalculate 1 CompleteCalc; 
  val ((pt,_),_) = get_calc 1;
  show_pt pt;
 
@@ -1022,7 +1022,7 @@
    ("Test", ["sqroot-test","univariate","equation","test"],
     ["Test","squ-equ-test-subpbl1"]))];
  Iterator 1; moveActiveRoot 1;
- autoCalculate' 1 CompleteCalc;
+ autoCalculate 1 CompleteCalc;
  val ((pt,_),_) = get_calc 1;
  show_pt pt;
 
@@ -1052,7 +1052,7 @@
 	   "solveFor x","solutions L"], 
   ("RatEq",["univariate","equation"],["no_met"]))];
 Iterator 1; moveActiveRoot 1;
-autoCalculate' 1 CompleteCalc; 
+autoCalculate 1 CompleteCalc; 
 val ((pt,_),_) = get_calc 1;
 val p = get_pos 1 1;
 val (Form f, tac, asms) = pt_extract (pt, p);
@@ -1092,35 +1092,35 @@
  fetchProposedTactic 1;
              (*ERROR get_calc 1 not existent*)
  setNextTactic 1 (Model_Problem );
- autoCalculate' 1 (Step 1); 
+ autoCalculate 1 (Step 1); 
  fetchProposedTactic 1;
  fetchProposedTactic 1;
 
  setNextTactic 1 (Add_Find "solutions L");
  setNextTactic 1 (Add_Find "solutions L");
 
- autoCalculate' 1 (Step 1); 
- autoCalculate' 1 (Step 1); 
+ autoCalculate 1 (Step 1); 
+ autoCalculate 1 (Step 1); 
 
  setNextTactic 1 (Specify_Theory "Test");
  fetchProposedTactic 1;
- autoCalculate' 1 (Step 1); 
+ autoCalculate 1 (Step 1); 
 
- autoCalculate' 1 (Step 1); 
- autoCalculate' 1 (Step 1); 
- autoCalculate' 1 (Step 1); 
- autoCalculate' 1 (Step 1); 
+ autoCalculate 1 (Step 1); 
+ autoCalculate 1 (Step 1); 
+ autoCalculate 1 (Step 1); 
+ autoCalculate 1 (Step 1); 
 (*------------------------- end calc-head*)
 
  fetchProposedTactic 1;
  setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
- autoCalculate' 1 (Step 1); 
+ autoCalculate 1 (Step 1); 
 
  setNextTactic 1 (Rewrite_Set "Test_simplify");
  fetchProposedTactic 1;
- autoCalculate' 1 (Step 1); 
+ autoCalculate 1 (Step 1); 
 
- autoCalculate' 1 CompleteCalc; 
+ autoCalculate 1 CompleteCalc; 
  val ((pt,_),_) = get_calc 1;
  val p = get_pos 1 1;
  val (Form f, tac, asms) = pt_extract (pt, p);
@@ -1136,9 +1136,9 @@
     ["Test","squ-equ-test-subpbl1"]))];
  Iterator 1;
  moveActiveRoot 1;
- autoCalculate' 1 CompleteCalcHead;
- autoCalculate' 1 (Step 1);
- autoCalculate' 1 (Step 1);
+ autoCalculate 1 CompleteCalcHead;
+ autoCalculate 1 (Step 1);
+ autoCalculate 1 (Step 1);
  appendFormula 1 "-1 + x = 0" (*|> Future.join*);
  (*... returns calcChangedEvent with*)
  val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
@@ -1159,9 +1159,9 @@
     ["Test","squ-equ-test-subpbl1"]))];
  Iterator 1;
  moveActiveRoot 1;
- autoCalculate' 1 CompleteCalcHead;
- autoCalculate' 1 (Step 1);
- autoCalculate' 1 (Step 1);
+ autoCalculate 1 CompleteCalcHead;
+ autoCalculate 1 (Step 1);
+ autoCalculate 1 (Step 1);
  appendFormula 1 "x - 1 = 0" (*|> Future.join*);
  val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
  getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
@@ -1182,9 +1182,9 @@
     ["Test","squ-equ-test-subpbl1"]))];
  Iterator 1;
  moveActiveRoot 1;
- autoCalculate' 1 CompleteCalcHead;
- autoCalculate' 1 (Step 1);
- autoCalculate' 1 (Step 1);
+ autoCalculate 1 CompleteCalcHead;
+ autoCalculate 1 (Step 1);
+ autoCalculate 1 (Step 1);
  appendFormula 1 "x = 1" (*|> Future.join*);
  (*... returns calcChangedEvent with*)
  val (unc, del, gen) = (([1],Res), ([1],Res), ([3,2],Res));
@@ -1206,9 +1206,9 @@
     ["Test","squ-equ-test-subpbl1"]))];
  Iterator 1;
  moveActiveRoot 1;
- autoCalculate' 1 CompleteCalcHead;
- autoCalculate' 1 (Step 1);
- autoCalculate' 1 (Step 1);
+ autoCalculate 1 CompleteCalcHead;
+ autoCalculate 1 (Step 1);
+ autoCalculate 1 (Step 1);
  appendFormula 1 "x - 4711 = 0" (*|> Future.join*);
  (*... returns <ERROR> no derivation found </ERROR>*)
 
@@ -1228,7 +1228,7 @@
     ["Test","squ-equ-test-subpbl1"]))];
  Iterator 1;
  moveActiveRoot 1;
- autoCalculate' 1 CompleteCalc;
+ autoCalculate 1 CompleteCalc;
  moveActiveFormula 1 ([2],Res);
  replaceFormula 1 "-1 + x = 0" (*i.e. repeats input*);
  (*... returns <ERROR> formula not changed </ERROR>*)
@@ -1249,7 +1249,7 @@
     ["Test","squ-equ-test-subpbl1"]))];
  Iterator 2;
  moveActiveRoot 2;
- autoCalculate' 2 CompleteCalc;
+ autoCalculate 2 CompleteCalc;
  moveActiveFormula 2 ([2],Res);
  replaceFormula 2 "-1 + x = 0" (*i.e. repeats input*);
  (*... returns <ERROR> formula not changed </ERROR>*)
@@ -1274,7 +1274,7 @@
     ["Test","squ-equ-test-subpbl1"]))];
  Iterator 1;
  moveActiveRoot 1;
- autoCalculate' 1 CompleteCalc;
+ autoCalculate 1 CompleteCalc;
  moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
  replaceFormula 1 "x - 1 = 0"; (*<-------------------------------------*)
  (*... returns calcChangedEvent with*)
@@ -1308,7 +1308,7 @@
     ["Test","squ-equ-test-subpbl1"]))];
  Iterator 1;
  moveActiveRoot 1;
- autoCalculate' 1 CompleteCalc;
+ autoCalculate 1 CompleteCalc;
  moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
  replaceFormula 1 "x = 1"; (*<-------------------------------------*)
  (*... returns calcChangedEvent with ...*)
@@ -1340,7 +1340,7 @@
     ["Test","squ-equ-test-subpbl1"]))];
  Iterator 1;
  moveActiveRoot 1;
- autoCalculate' 1 CompleteCalc;
+ autoCalculate 1 CompleteCalc;
  moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
  replaceFormula 1 "x - 4711 = 0"; 
  (*... returns <ERROR> no derivation found </ERROR>*)
@@ -1362,9 +1362,9 @@
   ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
 Iterator 1;
 moveActiveRoot 1;
-autoCalculate' 1 CompleteCalcHead;
-autoCalculate' 1 (Step 1);
-autoCalculate' 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
+autoCalculate 1 CompleteCalcHead;
+autoCalculate 1 (Step 1);
+autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
 appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*); (*<<<<<<<=========================*)
 (* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
   would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
@@ -1414,7 +1414,7 @@
     get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", ""))
   then () else error "inputFillFormula changed 11";
 
-autoCalculate' 1 CompleteCalc;
+autoCalculate 1 CompleteCalc;
 
 "~~~~~ final check: the input formula is inserted as it would have been correct from beginning";
 val ((pt, _),_) = get_calc 1;
@@ -1444,8 +1444,8 @@
 moveActiveRoot 1;
 moveActiveFormula 1 ([],Pbl);
 replaceFormula 1 "Simplify (5 * x / (4 * y) + 3 * x / (4 * y))";
-autoCalculate' 1 CompleteCalcHead;
-autoCalculate' 1 (Step 1);
+autoCalculate 1 CompleteCalcHead;
+autoCalculate 1 (Step 1);
 appendFormula 1 "8 * x / (8 * y)" (*|> Future.join*);
 (*<CALCMESSAGE> no derivation found </CALCMESSAGE> 
 --- but in BridgeLog Java <=> SML:
@@ -1463,7 +1463,7 @@
   ["diff","differentiate_on_R"]))]; (*<<<======= EP is directly in script*)
 Iterator 1;
 moveActiveRoot 1;
-autoCalculate' 1 CompleteCalc;
+autoCalculate 1 CompleteCalc;
 val ((pt,p),_) = get_calc 1; show_pt pt;
 
 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";
@@ -1477,9 +1477,9 @@
   ["diff","after_simplification"]))]; (*<<<======= EP is in a ruleset*)
 Iterator 1;
 moveActiveRoot 1;
-autoCalculate' 1 CompleteCalcHead;
-autoCalculate' 1 (Step 1); fetchProposedTactic 1;
-autoCalculate' 1 (Step 1); fetchProposedTactic 1;
+autoCalculate 1 CompleteCalcHead;
+autoCalculate 1 (Step 1); fetchProposedTactic 1;
+autoCalculate 1 (Step 1); fetchProposedTactic 1;
 (*
 <NEXTTAC>
   <CALCID> 1 </CALCID>
@@ -1514,7 +1514,7 @@
 stepOnErrorPatterns 1; (*--> calcChanged, rule calls getTactic and displays it *)
 (* then --- UC errpat, fillpat by input ---*)
 *)
-autoCalculate' 1 CompleteCalc;
+autoCalculate 1 CompleteCalc;
 val ((pt,p),_) = get_calc 1; show_pt pt;
 (*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*)