*}

 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

 *}

 ML {*

 ML {*

 *}

 "=(5)= transfer of non-local assumptions from sub-met to root-met";

 ML {*

 (*del*)terms2strs (get_assumptions_ pt p);

 val t = str2term "precond_rootmet x";

 get_assumptions_ pt p = [(*precond_rootmet, precond_submet, sub_asm_out, sub_res*)];

 val SOME (s, t') = eval_precond_rootmet "precond_rootmet_" 0 t @{theory};

 (*del*)terms2strs (get_assumptions_ pt p);

 term2str t'

 terms2strs (get_assumptions_ pt p);

 *}

 *}

 ML {*

 ML {*

 *}

 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt=Check_P["sqroot-test","univariate","equation","test"*)

 ML {*

 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

 *}

 *}

 ML {*

 ML {*

 *}

 "=(6)= assumptions collected during lucas-interpretation for proving postcondition";

 ML {*

 get_assumptions_ pt p = [(*precond_rootmet, precond_submet, sub_asm_out, sub_res, root_res*)];

 terms2strs (get_assumptions_ pt p);

 *}

 *}

 ML {*

 (*############################################################################*)

 *}

 ML {*

 (*Minisubplb/500-met-sub-to-root.sml*)

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

 val (dI',pI',mI') =

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

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

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)

 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["linear", "univariate", "equation", "test"]*)

 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)

 val (p,_,f,nxt,_,pt) = me nxt p'' [] pt''; (*nxt = Rewrite_Set_Inst isolate_bdv*);

 get_ctxt pt p |> is_e_ctxt;       (*false*)

 val ctxt = get_ctxt pt p; 

 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";

 get_loc pt p |> snd |> is_e_ctxt; (*false*)

 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*);

 get_ctxt pt p |> is_e_ctxt;       (*false*)

 val ctxt = get_ctxt pt p; 

 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";

 get_loc pt p |> snd |> is_e_ctxt; (*false*)

 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *);

 val (pt'''', p'''') = (pt, p);

 *}

 ML {*

 locatetac tac (pt,p)

 *}

 ML {*

 "~~~~~ fun me, args:"; val (_,tac) = nxt;

 val (pt, p) = case locatetac tac (pt,p) of

 	("ok", (_, _, ptp))  => ptp | _ => error "script.sml locatetac";

 *}

 ML {*

 show_pt pt; (*...(([3], Res), [x = 1])]... back in root, OK *)

 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))

 val pIopt = get_pblID (pt,ip); (*= SOME ["sqroot-test", "univariate", ...]*)

 tacis; (*= []*)

 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)

 *}

 ML {*

 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);

 val thy' = get_obj g_domID pt (par_pblobj pt p);

 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)

 "~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'), (sc as Script (h $ body)), 

 	                               (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);

 val ctxt = get_ctxt pt pos

 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";

 l; (*= [R, R, D, L, R]*)

 "~~~~~ fun nstep_up, args:"; val (thy, ptp, (Script sc), E, l, ay, a, v) =

                                  (thy, ptp, sc, E, l, Skip_, a, v);

 1 < length l; (*true*)

 val up = drop_last l;

 go up sc; (* = Const ("HOL.Let", *)

 *}

 ML {*

 "~~~~~ fun nxt_up, args:"; val (thy, ptp, (scr as (Script sc)), E, l, ay,

                                       (t as Const ("HOL.Let",_) $ _), a, v) =

                             (thy, ptp, (Script sc), E, up, ay, (go up sc), a, v);

 ay = Napp_; (*false*)

 val up = drop_last l;

 val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc;

 val i = mk_Free (i, T);

 val E = upd_env E (i, v);

 body; (*= Const ("Script.Check'_elementwise"*)

 "~~~~~ fun appy, args:"; val ((thy as (th,sr)), (pt, p), E, l, t, a, v)=

                               (thy, ptp, E, (up@[R,D]), body, a, v);

 handle_leaf "next  " th sr E a v t; (*= (NONE, STac (Const ("Script.Check'_elementwise"*)

 val (a', STac stac) = handle_leaf "next  " th sr E a v t;

 "~~~~~ fun stac2tac_, args:"; val (pt, thy, (Const("Script.Check'_elementwise",_) $ _ $ 

 		(set as Const ("Set.Collect",_) $ Abs (_,_,pred)))) = (pt, (assoc_thy th), stac);

 (*2011 changed ^^^^^   *)

 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*WAS nxt = ("Empty_Tac", Empty_Tac)*)

 if nxt = ("Check_elementwise", Check_elementwise "Assumptions") then ()

 else error "Check_elementwise changed; after switch sub-->root-method"

 *}