val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)

 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow> Add_Given "functionTerm (x \<up> 2 + 1)"*)

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

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

 val (p''',_,f,nxt''',_,pt''') = me nxt p c pt; (*nxt'''= Specify_Method ["diff", "integration"]*)

 (*/------------------- step into me Specify_Method ["diff", "integration"] -----------------\*)

 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt''', p''', c, pt''');

       val (pt, p) = 

   	    (*Step.by_tactic is here for testing by me; do_next would suffice in me*)

   	    case Step.by_tactic tac (pt, p) of

   		    ("ok", (_, _, ptp)) => ptp

 val ("ok", ([(Apply_Method ["diff", "integration"], _, _)], _, _)) = (*case*) 

       Step.do_next p ((pt, Pos.e_pos'), []) (*of*);

 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))

   = (p, ((pt, Pos.e_pos'), []));

   (*if*) Pos.on_calc_end ip (*else*);

       val (_, probl_id, _) = Calc.references (pt, p);

 val _ =

       (*case*) tacis (*of*);

         (*if*) probl_id = Problem.id_empty (*else*);

 val ("ok", ([(Apply_Method ["diff", "integration"], _, _)], _, _)) =

       Step.switch_specify_solve p_ (pt, ip);

 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));

       (*if*) Pos.on_specification ([], state_pos) (*then*);

       Step.specify_do_next (pt, input_pos);

 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);

     val (_, (p_', tac)) = Specify.find_next_step ptp

     val ist_ctxt =  Ctree.get_loc pt (p, p_)

 val Tactic.Apply_Method mI =

     (*case*) tac (*of*);

 val ("ok", ([(Apply_Method ["diff", "integration"], _, _)], _, _)) =

   	    LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))

   	      ist_ctxt (pt, (p, p_'));

 "~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _)))

   = ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)),

   	      ist_ctxt, (pt, (p, p_')));

          val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*)

            PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)

          | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"

          val {ppc, ...} = MethodC.from_store ctxt mI;

          val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc

          val srls = LItool.get_simplifier (pt, pos)

          val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of

            (is as Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr)

          | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case init_pstate"

         val ini = LItool.implicit_take prog env;

         val pos = start_new_level pos

 val NONE =

         (*case*) ini (*of*);

 val Next_Step (iii, ccc, ttt) = (*case*) 

         LI.find_next_step prog (pt, (lev_dn p, Res)) is ctxt (*of*);

 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt)

   = (prog, (pt, (lev_dn p, Res)), is, ctxt);

       (*case*)

            scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);

 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))

   = ((prog, (ptp, ctxt)), (Pstate ist));

   (*if*) path = [] (*then*);

 val Accept_Tac (ttt, sss, ccc) =

            scan_dn cc (trans_scan_dn ist) (Program.body_of prog);

 "~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b))))

   = (cc, (trans_scan_dn ist), (Program.body_of prog));

 val Accept_Tac (ttt, sss, ccc) = (*case*)

            scan_dn cc (ist |> path_down [L, R]) e (*of*);

 "~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)

   = (cc, (ist |> path_down [L, R]), e);

     (*if*) Tactical.contained_in t (*else*);

 val (Program.Tac prog_tac, form_arg) =

       (*case*)  LItool.check_leaf "next  " ctxt eval (get_subst ist) t (*of*);

 val Accept_Tac (ttt, sss, ccc) =

            check_tac cc ist (prog_tac, form_arg);

 "~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg))

   = (cc, ist, (prog_tac, form_arg));

     val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac

 val _ =

     (*case*) m (*of*);

       (*case*)

 Solve_Step.check m (pt, p) (*of*);

 "~~~~~ fun check , args:"; val ((Tactic.Take str), (pt, pos as (p_, p))) = (m, (pt, p));

 (*+*)val ([0], Res) = pos; (*<<<-------------------------*)

 (*-------------------- stop step into me Specify_Method ["diff", "integration"] -------------*)

 (*\------------------- step into me Specify_Method ["diff", "integration"] -----------------/*)

 val (p,_,f,nxt,_,pt) = me nxt''' p''' c pt''';