(* Title:  tests the interface of isac's SML-kernel in accordance to 

            java-tests/isac.bridge.

    Author: Walther Neuper

    (c) copyright due to lincense terms.

 WN050707 ... if true, the test ist marked with a \label referring

 to the same UC in isac-docu.tex as the JUnit testcase.

 WN120210?not ME: added some labels, which are not among the above,

 repaired lost \label (s).

 theory Test_Some imports Build_Thydata begin 

 ML {* KEStore_Elems.set_ref_thy @{theory};

   fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*) *}

 ML_file "Frontend/use-cases.sml"

 *)

 "--------------------------------------------------------";

 "table of contents --------------------------------------";

 "--------------------------------------------------------";

 "within struct ------------------------------------------";

 "--------------------------------------------------------";

 "--------- encode ^ -> ^^^ ------------------------------";

 "--------------------------------------------------------";

 "exported from struct -----------------------------------";

 "--------------------------------------------------------";

 "--------- empty rootpbl --------------------------------";

 "--------- solve_linear as rootpbl FE -------------------";

 "--------- inspect the CalcTree No.1 with Iterator No.2 -";

 "--------- miniscript with mini-subpbl ------------------";

 "--------- mini-subpbl AUTOCALCULATE Step 1 -------------";

 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";

 "--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";

 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";

 "--------- mini-subpbl AUTO CompleteCalcHead ------------";

 "--------- solve_linear as rootpbl AUTO CompleteModel ---";

 "--------- setContext..Thy ------------------------------";

 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";

 "--------- rat-eq + subpbl: no_met, NO solution dropped -";

 "--------- tryMatchProblem, tryRefineProblem ------------";

 "--------- modifyCalcHead, resetCalcHead, modelProblem --";

 "--------- maximum-example, UC: Modeling an example -----";

 "--------- solve_linear from pbl-hierarchy --------------";

 "--------- solve_linear as in an algebra system (CAS)----";

 "--------- interSteps: on 'miniscript with mini-subpbl' -";

 "--------- getTactic, fetchApplicableTactics ------------";

 "--------- getAssumptions, getAccumulatedAsms -----------";

 "--------- arbitrary combinations of steps --------------";

 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";

 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";

 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";

 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";

 "--------- replaceFormula {SOL:MAN:FOR:replace} right----";

 "--------- replaceFormula {SOL:MAN:FOR:replace} other----";

 "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";

 "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";

 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";

 "--------- UC errpat add-fraction, fillpat by input --------------";

 "--------- UC errpat, fillpat step to Rewrite --------------------";

 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";

 "--------------------------------------------------------";

 "within struct ---------------------------------------------------";

 "within struct ---------------------------------------------------";

 "within struct ---------------------------------------------------";

 (*==================================================================

 "--------- encode ^ -> ^^^ ------------------------------";

 "--------- encode ^ -> ^^^ ------------------------------";

 "--------- encode ^ -> ^^^ ------------------------------";

 if encode "a^2+b^2=c^2" = "a^^^2+b^^^2=c^^^2" then ()

 else error "interface.sml: diff.behav. in encode ^ -> ^^^ ";

 if (decode o encode) "a^2+b^2=c^2" = "a^2+b^2=c^2" then ()

 else error "interface.sml: diff.behav. in de/encode ^ <-> ^^^ ";

 ==================================================================*)

 "exported from struct --------------------------------------------";

 "exported from struct --------------------------------------------";

 "exported from struct --------------------------------------------";

 (*------------ set at startup of the Kernel ----------------------*)

 reset_states ();  (*resets all state information in Kernel           *)

 (*----------------------------------------------------------------*)

 "--------- empty rootpbl --------------------------------";

 "--------- empty rootpbl --------------------------------";

 "--------- empty rootpbl --------------------------------";

  CalcTree [([], ("", [], []))];

  Iterator 1;

  moveActiveRoot 1;

  refFormula 1 (get_pos 1 1);

 (*WN.040222: stoert das sehr, dass e_domID etc. statt leer kommt ???*)

 DEconstrCalcTree 1;

 "--------- solve_linear as rootpbl FE -------------------";

 "--------- solve_linear as rootpbl FE -------------------";

 "--------- solve_linear as rootpbl FE -------------------";

  CalcTree      (*start of calculation, return No.1*)

      [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],

        ("Test", 

 	["LINEAR","univariate","equation","test"],

 	["Test","solve_linear"]))];

  Iterator 1;     (*create an active Iterator on CalcTree No.1*)

  moveActiveRoot 1;(*sets the CalcIterator No.1 at the root of CalcTree No.1*);

  refFormula 1 (get_pos 1 1)  (*gets CalcHead; model is still empty*);

  fetchProposedTactic 1 (*by using Iterator No.1*);

  setNextTactic 1 (Model_Problem); (*by using Iterator No.1*)

  autoCalculate' 1 (Step 1);

  refFormula 1 (get_pos 1 1)  (*model contains descriptions for all items*);

  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*);

  fetchProposedTactic 1;

  setNextTactic 1 (Add_Given "solveFor x");

  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);

  fetchProposedTactic 1;

  setNextTactic 1 (Specify_Theory "Test");

  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);

 (*-------------------------------------------------------------------------*)

  fetchProposedTactic 1;

  val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;

  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);

  val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;

 (*-------------------------------------------------------------------------*)

  fetchProposedTactic 1;

  val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;

  setNextTactic 1 (Apply_Method ["Test","solve_linear"]);

    (*ERROR.110620 <SETNEXTTACTIC>..<MESSAGE> end-of-calculation*)

  val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;

  is_complete_mod ptp;

  is_complete_spec ptp;

  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);

  fetchProposedTactic 1;

  setNextTactic 1 (Rewrite_Set "Test_simplify");

  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);

  val ((pt,_),_) = get_calc 1;

  val ip = get_pos 1 1;

  val (Form f, tac, asms) = pt_extract (pt, ip);

      (*exception just above means: 'ModSpec' has been returned: error anyway*)

  if term2str f = "[x = 1]" then () else 

  error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl";

 "--------- inspect the CalcTree No.1 with Iterator No.2 -";

 "--------- inspect the CalcTree No.1 with Iterator No.2 -";

 "--------- inspect the CalcTree No.1 with Iterator No.2 -";

 (*WN041118: inspection shifted to Iterator No.1, because others need pos'*)

  moveActiveRoot 1; 

  refFormula 1 ([],Pbl); getTactic 1 ([],Pbl);(*Error*)

  moveActiveDown 1; 

  refFormula 1 ([1],Frm); getTactic 1 ([1],Frm);(*Error*)

  moveActiveDown 1 ; 

  refFormula 1 ([1],Res); getTactic 1 ([1],Res);(*OK*) 

  (*getAssumption 1 ([1],Res); TODO.WN041217*)

  moveActiveDown 1 ; refFormula 1 ([2],Res);

  moveActiveCalcHead 1; refFormula 1 ([],Pbl);

  moveActiveDown 1;

  moveActiveDown 1;

  moveActiveDown 1;

  if get_pos 1 1 = ([2], Res) then () else 

  error "FE-interface.sml: diff.behav. in a inspect 1 with Iterator 2";

  moveActiveDown 1; refFormula 1 ([], Res);

  if get_pos 1 1 = ([], Res) then () else 

  error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2";

  moveActiveCalcHead 1; refFormula 1 ([],Pbl);

 DEconstrCalcTree 1;

 "--------- miniscript with mini-subpbl ------------------";

 "--------- miniscript with mini-subpbl ------------------";

 "--------- miniscript with mini-subpbl ------------------";

 (*WN120210?not ME:\label{SOLVE:MANUAL:TACTIC:enter} UC 30.3.2.1 p.175 !!!!!NOT IMPL IN FE*)

 "=== this sequence of fun-calls resembles fun me ===";

  reset_states (); (*start of calculation, return No.1*)

  CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

    ("Test", ["sqroot-test","univariate","equation","test"],

     ["Test","squ-equ-test-subpbl1"]))];

  Iterator 1;

  moveActiveRoot 1; 

  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*)

  fetchProposedTactic 1;

  setNextTactic 1 (Add_Given "equality (x + 1 = 2)");

  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);

  fetchProposedTactic 1;

  setNextTactic 1 (Add_Find "solutions L");

  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);

  fetchProposedTactic 1;

  setNextTactic 1 (Specify_Problem 

 		      ["sqroot-test","univariate","equation","test"]);

  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);

  fetchProposedTactic 1;

  setNextTactic 1 (Apply_Method ["Test","squ-equ-test-subpbl1"]);

  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);

  fetchProposedTactic 1;

  setNextTactic 1 (Rewrite_Set "Test_simplify");

  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);

  fetchProposedTactic 1;

  setNextTactic 1 (Model_Problem );

  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);

  fetchProposedTactic 1;

  setNextTactic 1 (Add_Given "solveFor x");

  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);

  fetchProposedTactic 1;

  setNextTactic 1 (Specify_Theory "Test");

  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);

 "2-----------------------------------------------------------------";

  fetchProposedTactic 1;

  setNextTactic 1 (Specify_Method ["Test","solve_linear"]);

  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);

  fetchProposedTactic 1;

  setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));

  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);

  fetchProposedTactic 1;

  setNextTactic 1 (Check_Postcond ["LINEAR","univariate","equation","test"]);

  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);

  val xml = fetchProposedTactic 1;

  setNextTactic 1 (Check_Postcond 

 		      ["sqroot-test","univariate","equation","test"]);

  autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);

  val ((pt,_),_) = get_calc 1;

  val str = pr_ptree pr_short pt;

  writeln str;

  val ip = get_pos 1 1;

  val (Form f, tac, asms) = pt_extract (pt, ip);

      (*exception just above means: 'ModSpec' has been returned: error anyway*)

  if term2str f = "[x = 1]" then () else 

  error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";

  DEconstrCalcTree 1;

 "--------- mini-subpbl AUTOCALCULATE Step 1 -------------";

 "--------- mini-subpbl AUTOCALCULATE Step 1 -------------";

 "--------- mini-subpbl AUTOCALCULATE Step 1 -------------";

 (*WN120210?not ME:\label{SOLVE:AUTO:one} UC 30.3.3.2 p.176*)

  CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

    ("Test", ["sqroot-test","univariate","equation","test"],

     ["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);

  (*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);

  (*------------------------------------*)

 (* default_print_depth 13; get_calc 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);

  (*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);

  (*finish subproblem*)

  autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);

  (*finish problem*)

  autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1); 

  (*this checks the test for correctness..*)

  val ((pt,_),_) = get_calc 1;

  val p = get_pos 1 1;

  val (Form f, tac, asms) = pt_extract (pt, p);

  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 

  error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";

  DEconstrCalcTree 1;

 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";

 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";

 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";

 (*WN120210?not ME:\label{SPECIFY:START:auto} UC 30.2.4.2 p.174*)

  CalcTree

      [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],

        ("Test", 

 	["LINEAR","univariate","equation","test"],

 	["Test","solve_linear"]))];

  Iterator 1;

  moveActiveRoot 1;

 getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 999 false;

  autoCalculate' 1 CompleteCalc; 

  val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));

  getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;

  val ((pt,_),_) = get_calc 1;

  val p = get_pos 1 1;

  val (Form f, tac, asms) = pt_extract (pt, p);

  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 

  error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE ";

 DEconstrCalcTree 1;

 "--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";

 "--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";

 "--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";

 (* ERROR: error in kernel ?? *)

  CalcTree

      [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],

        ("Test", 

 	["LINEAR","univariate","equation","test"],

 	["Test","solve_linear"]))];

  Iterator 1;

  moveActiveRoot 1;

  autoCalculate' 1 CompleteCalcHead;

  refFormula 1 (get_pos 1 1);

  val ((pt,p),_) = get_calc 1;

  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 ";

 DEconstrCalcTree 1;

 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";

 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";

 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";

 (*WN120210?not ME:\label{SPECIFY:START:auto} UC 30.2.4.2 p.174*)

  CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

    ("Test", ["sqroot-test","univariate","equation","test"],

     ["Test","squ-equ-test-subpbl1"]))];

  Iterator 1;

  moveActiveRoot 1;

  autoCalculate' 1 CompleteCalc;

  val ((pt,p),_) = get_calc 1; show_pt pt;

 (*

 getTactic 1 ([1],Frm);

 getTactic 1 ([1],Res);

 initContext 1 Thy_ ([1],Res);

 *)

  (*... returns calcChangedEvent with*)

  val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));

  getFormulaeFromTo 1 unc gen 0 (*only result*) false;

  getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;

  getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;

  val ((pt,_),_) = get_calc 1;

  val p = get_pos 1 1;

  val (Form f, tac, asms) = pt_extract (pt, p);

  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 

  error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";

 DEconstrCalcTree 1;

 "--------- mini-subpbl AUTO CompleteCalcHead ------------";

 "--------- mini-subpbl AUTO CompleteCalcHead ------------";

 "--------- mini-subpbl AUTO CompleteCalcHead ------------";

  CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

    ("Test", ["sqroot-test","univariate","equation","test"],

     ["Test","squ-equ-test-subpbl1"]))];

  Iterator 1;

  moveActiveRoot 1;

  autoCalculate' 1 CompleteCalcHead;

 val ((Nd (PblObj {env = NONE, fmz = (fm, ("Test", pblID, metID)), loc = (SOME (env, ctxt1), NONE), 

       cell = NONE, ctxt = ctxt2, meth,

       spec = ("Test", ["sqroot-test", "univariate", "equation", "test"], 

         ["Test", "squ-equ-test-subpbl1"]), 

       probl, branch = TransitiveB, origin, ostate = Incomplete, result}, []),

    ([], Met)), []) = get_calc 1;

 if length meth = 3 andalso length probl = 3 (*just some items tested*) then () 

 else error "--- mini-subpbl AUTO CompleteCalcHead ---";

 DEconstrCalcTree 1;

 "--------- solve_linear as rootpbl AUTO CompleteModel ---";

 "--------- solve_linear as rootpbl AUTO CompleteModel ---";

 "--------- solve_linear as rootpbl AUTO CompleteModel ---";

  CalcTree

      [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],

        ("Test", 

 	["LINEAR","univariate","equation","test"],

 	["Test","solve_linear"]))];

  Iterator 1;

  moveActiveRoot 1;

  autoCalculate' 1 CompleteModel;  

  refFormula 1 (get_pos 1 1);

 setProblem 1 ["LINEAR","univariate","equation","test"];

 val pos = get_pos 1 1;

 setContext 1 pos (kestoreID2guh Pbl_["LINEAR","univariate","equation","test"]);

  refFormula 1 (get_pos 1 1);

 setMethod 1 ["Test","solve_linear"];

 setContext 1 pos (kestoreID2guh Met_ ["Test","solve_linear"]);

  refFormula 1 (get_pos 1 1);

  val ((pt,_),_) = get_calc 1;

  if get_obj g_spec pt [] = ("e_domID", 

 			    ["LINEAR", "univariate","equation","test"],

 			    ["Test","solve_linear"]) then ()

  else error "FE-interface.sml: diff.behav. in setProblem, setMethod";

  autoCalculate' 1 CompleteCalcHead;

  refFormula 1 (get_pos 1 1); 

  autoCalculate' 1 CompleteCalc; 

  moveActiveDown 1;

  moveActiveDown 1;

  moveActiveDown 1;

  refFormula 1 (get_pos 1 1); 

  val ((pt,_),_) = get_calc 1;

  val p = get_pos 1 1;

  val (Form f, tac, asms) = pt_extract (pt, p);

  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 

  error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";

 DEconstrCalcTree 1;

 "--------- setContext..Thy ------------------------------";

 "--------- setContext..Thy ------------------------------";

 "--------- setContext..Thy ------------------------------";

  reset_states ();

  CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

   ("Test", ["sqroot-test","univariate","equation","test"],

    ["Test","squ-equ-test-subpbl1"]))];

  Iterator 1; moveActiveRoot 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);

  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);

  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";

  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";

  DEconstrCalcTree 1;

 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";

 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";

 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";

  CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

    ("Test", ["sqroot-test","univariate","equation","test"],

     ["Test","squ-equ-test-subpbl1"]))];

  Iterator 1; moveActiveRoot 1;

  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;

  writeln str;

  if str = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n"

  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;

  val ((pt,_),_) = get_calc 1;

  val str = pr_ptree pr_short pt;

  writeln str;

  autoCalculate' 1 CompleteCalc; (*das geht ohnehin !*);

  val ((pt,_),_) = get_calc 1;

  val p = get_pos 1 1;

  val (Form f, tac, asms) = pt_extract (pt, p);

  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 

  error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";

 DEconstrCalcTree 1;

 "--------- rat-eq + subpbl: no_met, NO solution dropped -";

 "--------- rat-eq + subpbl: no_met, NO solution dropped -";

 "--------- rat-eq + subpbl: no_met, NO solution dropped -";

  CalcTree

  [(["equality ((5*x)/(x - 2) - x/(x+2)=(4::real))", "solveFor x","solutions L"],

    ("RatEq", ["univariate","equation"], ["no_met"]))];

  Iterator 1;

  moveActiveRoot 1; 

  fetchProposedTactic 1;

  setNextTactic 1 (Model_Problem);

  autoCalculate' 1 (Step 1); fetchProposedTactic 1;

  setNextTactic 1 (Specify_Theory "RatEq");

  autoCalculate' 1 (Step 1); fetchProposedTactic 1;

  setNextTactic 1 (Specify_Problem ["rational","univariate","equation"]);

  autoCalculate' 1 (Step 1); fetchProposedTactic 1;

  setNextTactic 1 (Specify_Method ["RatEq","solve_rat_equation"]);

  autoCalculate' 1 (Step 1); fetchProposedTactic 1;

  setNextTactic 1 (Apply_Method ["RatEq","solve_rat_equation"]);

  autoCalculate' 1 (Step 1); fetchProposedTactic 1;

  setNextTactic 1 (Rewrite_Set "RatEq_simplify");

  autoCalculate' 1 (Step 1); fetchProposedTactic 1;

  setNextTactic 1 (Rewrite_Set "norm_Rational");

  autoCalculate' 1 (Step 1); fetchProposedTactic 1;

  setNextTactic 1 (Rewrite_Set "RatEq_eliminate");

  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;

  setNextTactic 1 (Model_Problem );

  autoCalculate' 1 (Step 1); fetchProposedTactic 1;

  setNextTactic 1 (Specify_Theory "PolyEq");

  autoCalculate' 1 (Step 1); fetchProposedTactic 1;

  setNextTactic 1 (Specify_Problem ["normalize","polynomial",

 				   "univariate","equation"]);

  autoCalculate' 1 (Step 1); fetchProposedTactic 1;

  setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);

  autoCalculate' 1 (Step 1); fetchProposedTactic 1;

  setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);

  autoCalculate' 1 (Step 1); fetchProposedTactic 1;

  setNextTactic 1 (Rewrite ("all_left",""));

  autoCalculate' 1 (Step 1); fetchProposedTactic 1;

  setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));

  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;

  setNextTactic 1 (Model_Problem );

  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> !!!*)

  setNextTactic 1 (Refine_Problem ["univariate","equation"]);

  (*------------------------------------------------------------------*)

  autoCalculate' 1 (Step 1); fetchProposedTactic 1;

  setNextTactic 1 (Specify_Method ["PolyEq","solve_d1_polyeq_equation"]);

  autoCalculate' 1 (Step 1); fetchProposedTactic 1;

  setNextTactic 1 (Apply_Method ["PolyEq","solve_d1_polyeq_equation"]);

  autoCalculate' 1 (Step 1); fetchProposedTactic 1;

  setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "d1_polyeq_simplify"));

  autoCalculate' 1 (Step 1); fetchProposedTactic 1;

  setNextTactic 1 (Rewrite_Set "polyeq_simplify");

  autoCalculate' 1 (Step 1); fetchProposedTactic 1;

  setNextTactic 1 Or_to_List;

  autoCalculate' 1 (Step 1); fetchProposedTactic 1;

  setNextTactic 1 (Check_elementwise "Assumptions"); 

  autoCalculate' 1 (Step 1); fetchProposedTactic 1;

  setNextTactic 1 (Check_Postcond ["degree_1","polynomial",

 				  "univariate","equation"]);

  autoCalculate' 1 (Step 1); fetchProposedTactic 1;

  setNextTactic 1 (Check_Postcond ["normalize","polynomial",

 				  "univariate","equation"]);

  autoCalculate' 1 (Step 1); fetchProposedTactic 1;

  setNextTactic 1 (Check_Postcond ["rational","univariate","equation"]);

  val (ptp,_) = get_calc 1;

  val (Form t,_,_) = pt_extract ptp;

  if get_pos 1 1 = ([], Res) andalso term2str t = "[x = -4 / 3]" then ()

  else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";

 DEconstrCalcTree 1;

 "--------- tryMatchProblem, tryRefineProblem ------------";

 "--------- tryMatchProblem, tryRefineProblem ------------";

 "--------- tryMatchProblem, tryRefineProblem ------------";

 (*{\bf\UC{Having \isac{} Refine the Problem

  * Automatically}\label{SPECIFY:refine-auto}\\} test match and refine with

  * x^^^2 + 4*x + 5 = 2

 see isac.bridge.TestSpecify#testMatchRefine*)

  CalcTree

  [(["equality (x^2 + 4*x + 5 = (2::real))", "solveFor x","solutions L"],

    ("Isac", 

     ["univariate","equation"],

     ["no_met"]))];

  Iterator 1;

  moveActiveRoot 1; 

  fetchProposedTactic 1;

  setNextTactic 1 (Model_Problem );

  (*..this tactic should be done 'tacitly', too !*)

 (*

 autoCalculate' 1 CompleteCalcHead; 

 checkContext 1 ([],Pbl) "pbl_equ_univ";

 checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);

 *)

  autoCalculate' 1 (Step 1); 

  fetchProposedTactic 1;

  setNextTactic 1 (Add_Given "equality (x ^^^ 2 + 4 * x + 5 = (2::real))");

  autoCalculate' 1 (Step 1); 

  "--------- we go into the ProblemBrowser (_NO_ pblID selected) -";

 initContext 1 Pbl_ ([],Pbl);

 initContext 1 Met_ ([],Pbl);

  "--------- this match will show some incomplete items: ---------";

 checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);

 checkContext 1 ([],Pbl) (kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]);

  fetchProposedTactic 1;

  setNextTactic 1 (Add_Given "solveFor x"); autoCalculate' 1 (Step 1);

  fetchProposedTactic 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"]);

  "--------- this is a NOT matching model (some 'false': ---------";

 checkContext 1  ([],Pbl)(kestoreID2guh Pbl_ ["LINEAR","univariate","equation"]);

  "--------- find out a matching problem: ------------------------";

  "--------- find out a matching problem (FAILING: no new pbl) ---";

  refineProblem 1([],Pbl)(pblID2guh ["LINEAR","univariate","equation"]);

  "--------- find out a matching problem (SUCCESSFUL) ------------";

  refineProblem 1 ([],Pbl) (pblID2guh ["univariate","equation"]);

  "--------- tryMatch, tryRefine did not change the calculation -";

  "--------- this is done by <TRANSFER> on the pbl-browser: ------";

  setNextTactic 1 (Specify_Problem ["normalize","polynomial",

 				 "univariate","equation"]);

  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);

 (*and Specify_Theory skipped by fetchProposedTactic ?!?*)

  fetchProposedTactic 1;

  setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);

  autoCalculate' 1 (Step 1);

  fetchProposedTactic 1;

  setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);

  autoCalculate' 1 CompleteCalc;

  val ((pt,_),_) = get_calc 1;

  show_pt pt;

  val p = get_pos 1 1;

  val (Form f, tac, asms) = pt_extract (pt, p);

  if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else 

  error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";

 (*------------^^^-inserted-----------------------------------------------*)

 (*WN050904 the fetchProposedTactic's below may not have worked like that

   before, too, because there was no check*)

  fetchProposedTactic 1;

  setNextTactic 1 (Specify_Theory "PolyEq");

  autoCalculate' 1 (Step 1);

  fetchProposedTactic 1;

  setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);

  autoCalculate' 1 (Step 1);

  fetchProposedTactic 1;

  "--------- now the calc-header is ready for enter 'solving' ----";

  autoCalculate' 1 CompleteCalc;

  val ((pt,_),_) = get_calc 1;

  rootthy pt;

  show_pt pt;

  val p = get_pos 1 1;

  val (Form f, tac, asms) = pt_extract (pt, p);

  if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else 

  error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";

 DEconstrCalcTree 1;

 "--------- modifyCalcHead, resetCalcHead, modelProblem --";

 "--------- modifyCalcHead, resetCalcHead, modelProblem --";

 "--------- modifyCalcHead, resetCalcHead, modelProblem --";

  CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

    ("Test", ["sqroot-test","univariate","equation","test"],

     ["Test","squ-equ-test-subpbl1"]))];

  Iterator 1;

  moveActiveRoot 1; 

  modifyCalcHead 1 (([],Pbl),(*the position from refFormula*)

 		  "solve (x+1=2, x)",(*the headline*)

 		  [Given ["equality (x+1=(2::real))", "solveFor x"],

 		   Find ["solutions L"](*,Relate []*)],

 		  Pbl, 

 		  ("Test", 

 		   ["sqroot-test","univariate","equation","test"],

 		   ["Test","squ-equ-test-subpbl1"]));

 val ((Nd (PblObj {env = NONE,

                   fmz = (fm, tpm),

                   loc = (SOME scrst_ctxt, NONE),

                   ctxt,

                   cell = NONE,

                   meth,

                   spec = (thy,

                           ["sqroot-test", "univariate", "equation", "test"],

                           ["Test", "squ-equ-test-subpbl1"]),

                   probl,

                   branch = TransitiveB,

                   origin,

                   ostate = Incomplete,

                   result},

                []),

          ([], Pbl)),

       []) = get_calc 1;

 (*WN110622: is the same as in 2002, but shouldn't be probl = [3 items?]*)

 if length meth = 0 andalso length probl = 0 (*just some items tested*) then () 

 else error "--- modifyCalcHead, resetCalcHead, modelProblem 1 --";

 resetCalcHead 1;

 modelProblem 1;

 get_calc 1;

 val ((Nd (PblObj {env = NONE,

                   fmz = (fm, tpm),

                   loc = (SOME scrst_ctxt, NONE),

                   ctxt,

                   cell = NONE,

                   meth,

                   spec = ("e_domID", ["e_pblID"], ["e_metID"]),

                   probl,

                   branch = TransitiveB,

                   origin,

                   ostate = Incomplete,

                   result},

                []),

          ([], Pbl)),

       []) = get_calc 1;

 if length meth = 3 andalso length probl = 3 (*just some items tested*) then () 

 else error "--- modifyCalcHead, resetCalcHead, modelProblem 2 --";

 "--------- maximum-example, UC: Modeling an example -----";

 "--------- maximum-example, UC: Modeling an example -----";

 "--------- maximum-example, UC: Modeling an example -----";

 (* {\bf\UC{Editing the Model}\label{SPECIFY:enter}\label{SPECIFY:check}\\}

 see isac.bridge.TestModel#testEditItems

 *)

  val elems = ["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",

 	      "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",

 	      "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",

 	      "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",

 	      (*^^^ these are the elements for the root-problem (in variants)*)

               (*vvv these are elements required for subproblems*)

 	      "boundVariable a","boundVariable b","boundVariable alpha",

 	      "interval {x::real. 0 <= x & x <= 2*r}",

 	      "interval {x::real. 0 <= x & x <= 2*r}",

 	      "interval {x::real. 0 <= x & x <= pi}",

 	      "errorBound (eps=(0::real))"]

  (*specifying is not interesting for this example*)

  val spec = ("DiffApp", ["maximum_of","function"], 

 	     ["DiffApp","max_by_calculus"]);

  (*the empty model with descriptions for user-guidance by Model_Problem*)

  val empty_model = [Given ["fixedValues []"],

 		    Find ["maximum", "valuesFor"],

 		    Relate ["relations []"]]; 

  DEconstrCalcTree 1;

 "#################################################################";

  CalcTree [(elems, spec)];

  Iterator 1;

  moveActiveRoot 1; 

  refFormula 1 (get_pos 1 1);

  (*this gives a completely empty model*) 

  fetchProposedTactic 1;

 (*fill the CalcHead with Descriptions...*)

  setNextTactic 1 (Model_Problem );

  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 !!!!!!!!!!!!!*)

  (*input of two items, 'fixedValues [r=Arbfix]' and 'maximum b'...*)

  modifyCalcHead 1 (([],Pbl) (*position, from previous refFormula*),

 		  "Problem (DiffApp.thy, [maximum_of, function])",

 		  (*the head-form ^^^ is not used for input here*)

 		  [Given ["fixedValues [r=Arbfix]"(*new input*)],

 		   Find ["maximum b"(*new input*), "valuesFor"], 

 		   Relate ["relations"]],

 		  (*input (Arbfix will dissappear soon)*)

 		  Pbl (*belongsto*),

 		  e_spec (*no input to the specification*));

  (*the user does not know, what 'superfluous' for 'maximum b' may mean

   and asks what to do next*)

  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);

  (*this input completes the model*)

  modifyCalcHead 1 (([],Pbl), "not used here",

 		  [Given ["fixedValues [r=Arbfix]"],

 		   Find ["maximum A", "valuesFor [a,b]"(*new input*)], 

 		   Relate ["relations [A=a*b, \

 			   \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, e_spec);

  (*specification is not interesting and should be skipped by the dialogguide;

    !!!!!!!!!!!!!!!!!!!! input of ONE part at a time !!!!!!!!!!!!!!!!!!!!!!*)

  modifyCalcHead 1 (([],Pbl), "not used here",

 		  [Given ["fixedValues [r=Arbfix]"],

 		   Find ["maximum A", "valuesFor [a,b]"(*new input*)], 

 		   Relate ["relations [A=a*b, \

 			   \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, 

 		  ("DiffApp", ["e_pblID"], ["e_metID"]));

  modifyCalcHead 1 (([],Pbl), "not used here",

 		  [Given ["fixedValues [r=Arbfix]"],

 		   Find ["maximum A", "valuesFor [a,b]"(*new input*)], 

 		   Relate ["relations [A=a*b, \

 			   \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, 

 		  ("DiffApp", ["maximum_of","function"], 

 		   ["e_metID"]));

  modifyCalcHead 1 (([],Pbl), "not used here",

 		  [Given ["fixedValues [r=Arbfix]"],

 		   Find ["maximum A", "valuesFor [a,b]"(*new input*)], 

 		   Relate ["relations [A=a*b, \

 			   \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, 

 		  ("DiffApp", ["maximum_of","function"], 

 		   ["DiffApp","max_by_calculus"]));

  (*this final calcHead now has STATUS 'complete' !*)

  DEconstrCalcTree 1;

 "--------- solve_linear from pbl-hierarchy --------------";

 "--------- solve_linear from pbl-hierarchy --------------";

 "--------- solve_linear from pbl-hierarchy --------------";

  val (fmz, sp) = ([], ("", ["LINEAR","univariate","equation","test"], []));

  CalcTree [(fmz, sp)];

  Iterator 1; moveActiveRoot 1;

  refFormula 1 (get_pos 1 1);

  modifyCalcHead 1 (([],Pbl),"solve (1+-1*2+x=(0::real))",

 		  [Given ["equality (1+-1*2+x=(0::real))", "solveFor x"],

 		   Find ["solutions L"]],

 		  Pbl, 

 		  ("Test", ["LINEAR","univariate","equation","test"],

 		   ["Test","solve_linear"]));

  autoCalculate' 1 CompleteCalc;

  refFormula 1 (get_pos 1 1);

  val ((pt,_),_) = get_calc 1;

  val p = get_pos 1 1;

  val (Form f, tac, asms) = pt_extract (pt, p);

  if term2str f = "[x = 1]" andalso p = ([], Res) 

    andalso terms2str asms = "[\"matches (?a = ?b) (1 + -1 * 2 + x = 0)\"]" then () 

  else error "FE-interface.sml: diff.behav. in from pbl -hierarchy";

  DEconstrCalcTree 1;

 "--------- solve_linear as in an algebra system (CAS)----";

 "--------- solve_linear as in an algebra system (CAS)----";

 "--------- solve_linear as in an algebra system (CAS)----";

 (*WN120210?not ME:\label{UC:cas-input} UC 30.1.2.5 p.168*)

  val (fmz, sp) = ([], ("", [], []));

  CalcTree [(fmz, sp)];

  Iterator 1; moveActiveRoot 1;

  modifyCalcHead 1 (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], []));

  autoCalculate' 1 CompleteCalc;

  refFormula 1 (get_pos 1 1);

  val ((pt,_),_) = get_calc 1;

  val p = get_pos 1 1;

  val (Form f, tac, asms) = pt_extract (pt, p);

  if term2str f = "[x = 1]" andalso p = ([], Res) 

    andalso terms2str asms = "[\"matches (?a = ?b) (1 + -1 * 2 + x = 0)\"]" then () 

  else error "FE-interface.sml: diff.behav. in from pbl -hierarchy";

 DEconstrCalcTree 1;

 "--------- interSteps: on 'miniscript with mini-subpbl' -";

 "--------- interSteps: on 'miniscript with mini-subpbl' -";

 "--------- interSteps: on 'miniscript with mini-subpbl' -";

  CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

    ("Test", ["sqroot-test","univariate","equation","test"],

     ["Test","squ-equ-test-subpbl1"]))];

  Iterator 1;

  moveActiveRoot 1;

  autoCalculate' 1 CompleteCalc; 

  val ((pt,_),_) = get_calc 1;

  show_pt pt;

  (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)

  interSteps 1 ([2],Res);

  val ((pt,_),_) = get_calc 1; show_pt pt (*new ([2,1],Frm)..([2,6],Res)*);

  val (unc, del, gen) = (([1],Res),([1],Res),([2,6],Res));

  getFormulaeFromTo 1 unc gen 1 false; 

  (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)

  interSteps 1 ([3,2],Res);

  val ((pt,_),_) = get_calc 1; show_pt pt (*new ([3,2,1],Frm)..([3,2,2],Res)*);

  val (unc, del, gen) = (([3,1],Res),([3,1],Res),([3,2,2],Res));

  getFormulaeFromTo 1 unc gen 1 false; 

  (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)

  interSteps 1 ([3],Res)  (*no new steps in subproblems*);

  val (unc, del, gen) = (([3],Pbl),([3],Pbl),([3,2],Res));

  getFormulaeFromTo 1 unc gen 1 false; 

  (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)

  interSteps 1 ([],Res)  (*no new steps in subproblems*);

  val (unc, del, gen) = (([],Pbl),([],Pbl),([4],Res));

  getFormulaeFromTo 1 unc gen 1 false; 

 DEconstrCalcTree 1;

 "--------- getTactic, fetchApplicableTactics ------------";

 "--------- getTactic, fetchApplicableTactics ------------";

 "--------- getTactic, fetchApplicableTactics ------------";

 (* compare test/../script.sml

 "----------- fun sel_rules ---------------------------------------";

 *)

  CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

    ("Test", ["sqroot-test","univariate","equation","test"],

     ["Test","squ-equ-test-subpbl1"]))];

  Iterator 1; moveActiveRoot 1;

  autoCalculate' 1 CompleteCalc;

  val ((pt,_),_) = get_calc 1;

  show_pt pt;

  (*UC\label{SOLVE:HIDE:getTactic} \label{SOLVE:AUTO:tactic} UC 30.3.3.1 p.176

 WN120210 not impl. in FE*)

  getTactic 1 ([],Pbl);

  getTactic 1 ([1],Res);

  getTactic 1 ([3],Pbl);

  getTactic 1 ([3,1],Frm);

  getTactic 1 ([3],Res);

  getTactic 1 ([],Res);

 (*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)

  fetchApplicableTactics 1 99999 ([],Pbl);

  fetchApplicableTactics 1 99999 ([1],Res);

  fetchApplicableTactics 1 99999 ([3],Pbl);

  fetchApplicableTactics 1 99999 ([3,1],Res);

  fetchApplicableTactics 1 99999 ([3],Res);

  fetchApplicableTactics 1 99999 ([],Res);

 DEconstrCalcTree 1;

 "--------- getAssumptions, getAccumulatedAsms -----------";

 "--------- getAssumptions, getAccumulatedAsms -----------";

 "--------- getAssumptions, getAccumulatedAsms -----------";

 CalcTree

 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",

 	   "solveFor x","solutions L"], 

   ("RatEq",["univariate","equation"],["no_met"]))];

 Iterator 1; moveActiveRoot 1;

 autoCalculate' 1 CompleteCalc; 

 val ((pt,_),_) = get_calc 1;

 val p = get_pos 1 1;

 val (Form f, tac, asms) = pt_extract (pt, p);

 (*============ inhibit exn WN120316 compare 2002--2011 ===========================

 if map term2str asms = 

  ["True |\n~ lhs ((3 + -1 * x + x ^^^ 2) * x =\n" ^

   "       1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x", "-6 * x + 5 * x ^^^ 2 = 0", 

   "lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x",

   "lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2", 

   "9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0"] 

 andalso term2str f = "[-6 * x + 5 * x ^^^ 2 = 0]" andalso p = ([], Res) then ()

 else error "TODO compare 2002--2011"; (*...data during test --- x / (x ^ 2 - 6 * x + 9) - 1...*)

 ============ inhibit exn WN120316 compare 2002--2011 ===========================*)

 if p = ([], Res) andalso term2str f = "[]" (*see WN120317.TODO dropped rateq*)

 andalso asms = [] (*STRANGE!, compare test --- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 ...*)

 then () else error "rlang.sml: diff.behav. in  Schalk I s.87 Bsp 55b [x = 6 / 5]";

 (*UC\label{SOLVE:HELP:assumptions} UC 30.3.5.1 p.178*)

 getAssumptions 1 ([3], Res);

 getAssumptions 1 ([5], Res);

 (*UC\label{SOLVE:HELP:assumptions-origin} UC 30.3.5.2 p.178

   WN0502 still without positions*)

 getAccumulatedAsms 1 ([3], Res);

 getAccumulatedAsms 1 ([5], Res);

 DEconstrCalcTree 1;

 "--------- arbitrary combinations of steps --------------";

 "--------- arbitrary combinations of steps --------------";

 "--------- arbitrary combinations of steps --------------";

  CalcTree      (*start of calculation, return No.1*)

      [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],

        ("Test", 

 	["LINEAR","univariate","equation","test"],

 	["Test","solve_linear"]))];

  Iterator 1; moveActiveRoot 1;

  fetchProposedTactic 1;

              (*ERROR get_calc 1 not existent*)

  setNextTactic 1 (Model_Problem );

  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); 

  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); 

 (*------------------------- end calc-head*)

  fetchProposedTactic 1;

  setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));

  autoCalculate' 1 (Step 1); 

  setNextTactic 1 (Rewrite_Set "Test_simplify");

  fetchProposedTactic 1;

  autoCalculate' 1 (Step 1); 

  autoCalculate' 1 CompleteCalc; 

  val ((pt,_),_) = get_calc 1;

  val p = get_pos 1 1;

  val (Form f, tac, asms) = pt_extract (pt, p);

  if term2str f = "[x = 1]" andalso p = ([], Res) then () else 

  error "FE-interface.sml: diff.behav. in combinations of steps";

 DEconstrCalcTree 1;

 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right"; (*UC 30.3.2.4 p.175*)

 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";

 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";

  CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

    ("Test", ["sqroot-test","univariate","equation","test"],

     ["Test","squ-equ-test-subpbl1"]))];

  Iterator 1;

  moveActiveRoot 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));

  getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;

  val ((pt,_),_) = get_calc 1;

  val p = get_pos 1 1;

  val (Form f, tac, asms) = pt_extract (pt, p);

  if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else 

  error "FE-interface.sml: diff.behav. in FORMULA:enter} right";

 DEconstrCalcTree 1;

 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other"; (*UC 30.3.2.4 p.175*)

 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";

 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";

  CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

    ("Test", ["sqroot-test","univariate","equation","test"],

     ["Test","squ-equ-test-subpbl1"]))];

  Iterator 1;

  moveActiveRoot 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;

  (*11 elements !!!*)

  val ((pt,_),_) = get_calc 1;

  val p = get_pos 1 1;

  val (Form f, tac, asms) = pt_extract (pt, p);

  if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else 

  error "FE-interface.sml: diff.behav. in FORMULA:enter} other";

 DEconstrCalcTree 1;

 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2"; (*UC 30.3.2.4 p.175*)

 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";

 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";

  CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

    ("Test", ["sqroot-test","univariate","equation","test"],

     ["Test","squ-equ-test-subpbl1"]))];

  Iterator 1;

  moveActiveRoot 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));

  getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;

  (*6 elements !!!*)

  val ((pt,_),_) = get_calc 1;

  val p = get_pos 1 1;

  val (Form f, tac, asms) = pt_extract (pt, p);

  if term2str f = "x = 1" andalso p = ([3,2], Res) then () else 

  error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2";

 DEconstrCalcTree 1;

 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok"; (*UC 30.3.2.4 p.175*)

 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";

 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";

  CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

    ("Test", ["sqroot-test","univariate","equation","test"],

     ["Test","squ-equ-test-subpbl1"]))];

  Iterator 1;

  moveActiveRoot 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>*)

  val ((pt,_),_) = get_calc 1;

  val p = get_pos 1 1;

  val (Form f, tac, asms) = pt_extract (pt, p);

  if term2str f = "x + 1 + -1 * 2 = 0" andalso p = ([1], Res) then () else 

  error "FE-interface.sml: diff.behav. in FORMULA:enter} NOTok";

 DEconstrCalcTree 1;

 "--------- replaceFormula {SOL:MAN:FOR:replace} right----"; (*UC 30.3.2.5 p.176*)

 "--------- replaceFormula {SOL:MAN:FOR:replace} right----";

 "--------- replaceFormula {SOL:MAN:FOR:replace} right----";

 (*\label{SOLVE:MANUAL:FORMULA:replace}*)

  CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

    ("Test", ["sqroot-test","univariate","equation","test"],

     ["Test","squ-equ-test-subpbl1"]))];

  Iterator 1;

  moveActiveRoot 1;

  autoCalculate' 1 CompleteCalc;

  moveActiveFormula 1 ([2],Res);

  replaceFormula 1 "-1 + x = 0" (*i.e. repeats input*);

  (*... returns <ERROR> formula not changed </ERROR>*)

  val ((pt,_),_) = get_calc 1;

  val p = get_pos 1 1;

  val (Form f, tac, asms) = pt_extract (pt, p);

  if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else 

  error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";

  if map fst (get_interval ([2],Res) ([],Res) 9999 pt) = 

     [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),

      ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else

  error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2";

 (*WN050211 replaceFormula didn't work on second ctree: thus now tested...*)

  CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

    ("Test", ["sqroot-test","univariate","equation","test"],

     ["Test","squ-equ-test-subpbl1"]))];

  Iterator 2;

  moveActiveRoot 2;

  autoCalculate' 2 CompleteCalc;

  moveActiveFormula 2 ([2],Res);

  replaceFormula 2 "-1 + x = 0" (*i.e. repeats input*);

  (*... returns <ERROR> formula not changed </ERROR>*)

  val ((pt,_),_) = get_calc 2;

  val p = get_pos 2 1;

  val (Form f, tac, asms) = pt_extract (pt, p);

  if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else 

  error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";

  if map fst (get_interval ([2],Res) ([],Res) 9999 pt) = 

     [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),

      ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else

  error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b";

 DEconstrCalcTree 1;

 "--------- replaceFormula {SOL:MAN:FOR:replace} other----"; (*UC 30.3.2.5 p.176*)

 "--------- replaceFormula {SOL:MAN:FOR:replace} other----";

 "--------- replaceFormula {SOL:MAN:FOR:replace} other----";

 (*\label{SOLVE:MANUAL:FORMULA:replace}*)

  CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

    ("Test", ["sqroot-test","univariate","equation","test"],

     ["Test","squ-equ-test-subpbl1"]))];

  Iterator 1;

  moveActiveRoot 1;

  autoCalculate' 1 CompleteCalc;

  moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)

  replaceFormula 1 "x - 1 = 0"; (*<-------------------------------------*)

  (*... returns calcChangedEvent with*)

  val (unc, del, gen) = (([1],Res), ([4],Res), ([2],Res));

  getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;

  val ((pt,_),_) = get_calc 1;

  show_pt pt;

  val p = get_pos 1 1;

  val (Form f, tac, asms) = pt_extract (pt, p);

  if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else 

  error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1";

 (* for getting the list in whole length ...

 default_print_depth 99;map fst (get_interval ([1],Res) ([],Res) 9999 pt);default_print_depth 3;

    *)

  if map fst (get_interval ([1],Res) ([],Res) 9999 pt) = 

     [([1], Res), ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),

       ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2, 7], Res),

       ([2, 8], Res), ([2, 9], Res), ([2], Res)

 (*WN060727 {cutlevup->test_trans} removed: , 

       ([], Res)(*dropped, if test_trans doesnt stop at PblNd*)*)] then () else

  error "FE-interface.sml: diff.behav. in FORMULA:replace} other 2";

 DEconstrCalcTree 1;

 "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--"; (*UC 30.3.2.5 p.176*)

 "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";

 "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";

 (*\label{SOLVE:MANUAL:FORMULA:replace}*)

  CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

    ("Test", ["sqroot-test","univariate","equation","test"],

     ["Test","squ-equ-test-subpbl1"]))];

  Iterator 1;

  moveActiveRoot 1;

  autoCalculate' 1 CompleteCalc;

  moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)

  replaceFormula 1 "x = 1"; (*<-------------------------------------*)

  (*... returns calcChangedEvent with ...*)

  val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));

  getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;

  (*9 elements !!!*)

  val ((pt,_),_) = get_calc 1;

  show_pt pt; (*error: ...get_interval drops ([3,2],Res) ...*)

  val (t,_) = get_obj g_result pt [3,2]; term2str t;

   if map fst (get_interval ([1],Res) ([],Res) 9999 pt) = 

     [([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res),

       ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), 

       ([3,2],Res)] then () else

  error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 1";

  val p = get_pos 1 1;

  val (Form f, tac, asms) = pt_extract (pt, p);

  if term2str f = "x = 1" andalso p = ([3,2], Res) then () else 

  error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 2";

 DEconstrCalcTree 1;

 "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----"; (*UC 30.3.2.5 p.176*)

 "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";

 "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";

 (*\label{SOLVE:MANUAL:FORMULA:replace}*)

  CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

    ("Test", ["sqroot-test","univariate","equation","test"],

     ["Test","squ-equ-test-subpbl1"]))];

  Iterator 1;

  moveActiveRoot 1;

  autoCalculate' 1 CompleteCalc;

  moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)

  replaceFormula 1 "x - 4711 = 0"; 

  (*... returns <ERROR> no derivation found </ERROR>*)

  val ((pt,_),_) = get_calc 1;

  show_pt pt;

  val p = get_pos 1 1;

  val (Form f, tac, asms) = pt_extract (pt, p);

  if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else 

  error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";

 DEconstrCalcTree 1;

 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";

 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";

 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";

 reset_states ();

 CalcTree

 [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"], 

   ("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))*)

 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.

   results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>

   instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)

   val ((pt,pos), _) = get_calc 1;

   val p = get_pos 1 1;

   val (Form f, _, asms) = pt_extract (pt, p);

   if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso

     get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], 

       ("diff_sum", "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))

   then () else error "embed fun get_fillform changed 1";

 (*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================

 findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)

 (*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =

   d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)

   val ((pt,pos),_) = get_calc 1;

   val p = get_pos 1 1;

   val (Form f, _, asms) = pt_extract (pt, p);

   if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso

     get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"(*?!?*)))

   then ()

   else error "embed fun get_fillform changed 2";

 (* if we assume, that the fill-patterns are ordered such that the 1st has large gaps

    and the last has no gaps, then the number of fill-patterns would suffice

    for the DialogGuide to select appropriately. *)

 requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*)

   (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)

   val ((pt,pos),_) = get_calc 1;

   val p = get_pos 1 1;

   val (Form f, _, asms) = pt_extract (pt, p);

   if p = ([1], Res) andalso existpt [2] pt andalso

     term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso

     get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"))

   then () else error "embed fun get_fillform changed 3";

 inputFillFormula 1 "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)";(*<<<<<<<=====*)

   val ((pt, _),_) = get_calc 1;

   val p = get_pos 1 1;

   val (Form f, _, asms) = pt_extract (pt, p);

   if p = ([2], Res) andalso

     term2str f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)" andalso

     get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", ""))

   then () else error "inputFillFormula changed 11";

 autoCalculate' 1 CompleteCalc;

 "~~~~~ final check: the input formula is inserted as it would have been correct from beginning";

 val ((pt, _),_) = get_calc 1;

 val p = get_pos 1 1;

 val (Form f, _, asms) = pt_extract (pt, p);

 if p = ([], Res) andalso term2str f = "2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3"

 then () else error "inputFillFormula changed 12";

 show_pt pt;

 (*[

 (([], Frm), Diff (x ^^^ 2 + sin (x ^^^ 4), x)),

 (([1], Frm), d_d x (x ^^^ 2 + sin (x ^^^ 4))),

 (([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))),

 (([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)),       (*<<<<<<<=====*)

 (([3], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * (4 * x ^^^ (4 - 1))),

 (([4], Res), 2 * x ^^^ (2 - 1) + cos (x ^^^ 4) * (4 * x ^^^ (4 - 1))),

 (([5], Res), 2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3),

 (([], Res), 2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3)] *)

 ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)

 "--------- UC errpat add-fraction, fillpat by input --------------";

 "--------- UC errpat add-fraction, fillpat by input --------------";

 "--------- UC errpat add-fraction, fillpat by input --------------";

 (*cp from BridgeLog Java <=> SML*)

 reset_states ();

 CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];

 Iterator 1;

 moveActiveRoot 1;

 moveActiveFormula 1 ([],Pbl);

 replaceFormula 1 "Simplify (5 * x / (4 * y) + 3 * x / (4 * y))";

 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:

 <CALCMESSAGE> error pattern #addition-of-fractions# </CALCMESSAGE>*)

 "--------- UC errpat, fillpat step to Rewrite --------------------";

 "--------- UC errpat, fillpat step to Rewrite --------------------";

 "--------- UC errpat, fillpat step to Rewrite --------------------";

 (*TODO*)

 reset_states ();

 CalcTree

 [(["functionTerm ((x ^ 2) ^ 3 + sin (x ^ 4))",

    "differentiateFor x", "derivative f_f'"], 

   ("Isac", ["derivative_of","function"],

   ["diff","differentiate_on_R"]))]; (*<<<======= EP is directly in script*)

 Iterator 1;

 moveActiveRoot 1;

 autoCalculate' 1 CompleteCalc;

 val ((pt,p),_) = get_calc 1; show_pt pt;

 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";

 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";

 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";

 reset_states ();

 CalcTree

 [(["functionTerm ((x ^ 2) ^ 3 + sin (x ^ 4))",

    "differentiateFor x", "derivative f_f'"], 

   ("Isac", ["derivative_of","function"],

   ["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;

 (*

 <NEXTTAC>

   <CALCID> 1 </CALCID>

   <TACTICERRORPATTERNS>

     <STRINGLIST>

       <STRING> chain-rule-diff-both </STRING>

       <STRING> cancel </STRING>

     </STRINGLIST>

     <REWRITESETINSTTACTIC name="Rewrite_Set_Inst">

       <RULESET> norm_diff </RULESET>

       <SUBSTITUTION>

         <PAIR>

           <VARIABLE>

             <MATHML>

               <ISA> bdv </ISA>

             </MATHML>

           </VARIABLE>

           <VALUE>

             <MATHML>

               <ISA> x </ISA>

             </MATHML>

           </VALUE>

         </PAIR>

       </SUBSTITUTION>

     </REWRITESETINSTTACTIC>

   </TACTICERRORPATTERNS>

 </NEXTTAC>

 (*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*)

 stepToErrorPatterns 1; (*--> calcChanged, rule immediately calls... *)

 stepOnErrorPatterns 1; (*--> calcChanged, rule calls getTactic and displays it *)

 (* then --- UC errpat, fillpat by input ---*)

 *)

 autoCalculate' 1 CompleteCalc;

 val ((pt,p),_) = get_calc 1; show_pt pt;

 (*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*)