1.1 --- a/src/Tools/isac/MathEngBasic/applicable.sml Thu Dec 07 11:54:42 2023 +0100
1.2 +++ b/src/Tools/isac/MathEngBasic/applicable.sml Thu Dec 07 16:14:32 2023 +0100
1.3 @@ -20,7 +20,7 @@
1.4 (**)
1.5
1.6 datatype T =
1.7 - Yes of Tactic.T (* tactic is applicable at a certain position in the Ctree *)
1.8 + Yes of Tactic.T (* tactic is applicable at a certain position in the Ctree *)
1.9 | No of string (* tactic is NOT applicable *)
1.10
1.11 (**)end(**);
2.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Thu Dec 07 11:54:42 2023 +0100
2.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Thu Dec 07 16:14:32 2023 +0100
2.3 @@ -11,14 +11,15 @@
2.4 signature TACTIC =
2.5 sig
2.6 datatype T =
2.7 - Add_Find' of TermC.as_string * Model_Def.i_model | Add_Given' of TermC.as_string * Model_Def.i_model
2.8 - | Add_Relation' of TermC.as_string * Model_Def.i_model
2.9 + Add_Find' of TermC.as_string * Model_Def.i_model_POS
2.10 + | Add_Given' of TermC.as_string * Model_Def.i_model_POS
2.11 + | Add_Relation' of TermC.as_string * Model_Def.i_model_POS
2.12 (*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
2.13 - | Model_Problem' of Problem.id * Model_Def.i_model * Model_Def.i_model
2.14 - | Refine_Problem' of Problem.id * (Model_Def.i_model * Pre_Conds_Def.T)
2.15 - | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * MethodC.id * Model_Def.i_model
2.16 - | Specify_Method' of MethodC.id * Model_Def.o_model * Model_Def.i_model
2.17 - | Specify_Problem' of Problem.id * (bool * (Model_Def.i_model * Pre_Conds_Def.T))
2.18 + | Model_Problem' of Problem.id * Model_Def.i_model_POS * Model_Def.i_model_POS
2.19 + | Refine_Problem' of Problem.id * (Model_Def.i_model_POS * Pre_Conds_Def.T)
2.20 + | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * MethodC.id * Model_Def.i_model_POS
2.21 + | Specify_Method' of MethodC.id * Model_Def.o_model * Model_Def.i_model_POS
2.22 + | Specify_Problem' of Problem.id * (bool * (Model_Def.i_model_POS * Pre_Conds_Def.T))
2.23 | Specify_Theory' of ThyC.id
2.24 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
2.25 | Apply_Method' of MethodC.id * term option * Istate_Def.T * Proof.context
2.26 @@ -312,24 +313,24 @@
2.27 (** tactics for internal use **)
2.28
2.29 datatype T =
2.30 - Add_Find' of TermC.as_string * Model_Def.i_model | Add_Given' of TermC.as_string * Model_Def.i_model
2.31 - | Add_Relation' of TermC.as_string * Model_Def.i_model (* for Step.do_next *)
2.32 + Add_Find' of TermC.as_string * Model_Def.i_model_POS | Add_Given' of TermC.as_string * Model_Def.i_model_POS
2.33 + | Add_Relation' of TermC.as_string * Model_Def.i_model_POS (* for Step.do_next *)
2.34 (*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
2.35 | Model_Problem' of (* first step in specify-phase *)
2.36 Problem.id * (* id in the Know_Store *)
2.37 - Model_Def.i_model * (* the model for the Problem *)
2.38 - Model_Def.i_model (* the model for the method *)
2.39 - | Refine_Problem' of Problem.id * (Model_Def.i_model * Pre_Conds_Def.T)
2.40 + Model_Def.i_model_POS * (* the model for the Problem *)
2.41 + Model_Def.i_model_POS (* the model for the method *)
2.42 + | Refine_Problem' of Problem.id * (Model_Def.i_model_POS * Pre_Conds_Def.T)
2.43 | Refine_Tacitly' of
2.44 Problem.id * (* the original id in the Know_Store *)
2.45 Problem.id * (* the id of the refined Problem *)
2.46 ThyC.id * (* the id of the refined theory *)
2.47 MethodC.id * (* the id of the refined MethodC *)
2.48 - Model_Def.i_model (* RM 9.03: remains [] for Model_Problem recognizing its activation *)
2.49 - | Specify_Method' of MethodC.id * Model_Def.o_model * Model_Def.i_model
2.50 + Model_Def.i_model_POS (* RM 9.03: remains [] for Model_Problem recognizing its activation *)
2.51 + | Specify_Method' of MethodC.id * Model_Def.o_model * Model_Def.i_model_POS
2.52 | Specify_Problem' of Problem.id *
2.53 (bool * (* all preconditions evaluate to True *)
2.54 - (Model_Def.i_model * (* the model checked for the input id *)
2.55 + (Model_Def.i_model_POS * (* the model checked for the input id *)
2.56 Pre_Conds_Def.T)) (* individual preconditions marked true/false *)
2.57 | Specify_Theory' of ThyC.id
2.58 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
3.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Thu Dec 07 11:54:42 2023 +0100
3.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Thu Dec 07 16:14:32 2023 +0100
3.3 @@ -42,7 +42,7 @@
3.4 Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
3.5 | Ctree.PrfObj _ => raise ERROR "Math_Engine.set_method: case 2 uncovered"
3.6 in
3.7 - (pt, (complete, Pos.Met, hdf, I_Model.OLD_to_POS mits, where_, spec) : SpecificationC.T)
3.8 + (pt, (complete, Pos.Met, hdf, mits, where_, spec) : SpecificationC.T)
3.9 end
3.10
3.11 (* specify a new problem; WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem ' *)
3.12 @@ -59,7 +59,7 @@
3.13 Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
3.14 | Ctree.PrfObj _ => raise ERROR "set_problem: case 2 uncovered"
3.15 in
3.16 - (pt, (complete, Pos.Pbl, hdf, I_Model.OLD_to_POS pits, where_, spec) : SpecificationC.T)
3.17 + (pt, (complete, Pos.Pbl, hdf, pits, where_, spec) : SpecificationC.T)
3.18 end
3.19
3.20 fun set_theory tI ptp =
3.21 @@ -74,7 +74,7 @@
3.22 case Ctree.get_obj I pt p of
3.23 Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
3.24 | Ctree.PrfObj _ => raise ERROR "set_theory: case 2 uncovered"
3.25 - in (pt, (complete, Pos.Pbl, hdf, I_Model.OLD_to_POS pits, where_, spec) : SpecificationC.T) end;
3.26 + in (pt, (complete, Pos.Pbl, hdf, pits, where_, spec) : SpecificationC.T) end;
3.27
3.28 (* does several steps within one calculation as given by "type auto";
3.29 the steps may arbitrarily go into and leave different phases,
4.1 --- a/src/Tools/isac/Specify/Specify.thy Thu Dec 07 11:54:42 2023 +0100
4.2 +++ b/src/Tools/isac/Specify/Specify.thy Thu Dec 07 16:14:32 2023 +0100
4.3 @@ -26,6 +26,8 @@
4.4
4.5 ML \<open>
4.6 \<close> ML \<open>
4.7 +Refine.problem: theory -> Problem.id -> I_Model.T -> (Problem.id * (I_Model.T * Pre_Conds.T)) option
4.8 +\<close> ML \<open>
4.9
4.10 \<close> ML \<open>
4.11 \<close>
5.1 --- a/src/Tools/isac/Specify/i-model.sml Thu Dec 07 11:54:42 2023 +0100
5.2 +++ b/src/Tools/isac/Specify/i-model.sml Thu Dec 07 16:14:32 2023 +0100
5.3 @@ -53,7 +53,7 @@
5.4 (*probably unused in PIDE, thus-----v----v*)
5.5 val add_single: theory -> single_POS -> T_POS -> T_POS
5.6
5.7 - val make_tactic: m_field -> TermC.as_string * T -> Tactic.T
5.8 + val make_tactic: m_field -> TermC.as_string * T_POS -> Tactic.T
5.9
5.10 val descriptor: feedback -> descriptor
5.11 val descriptor_POS: feedback_POS -> descriptor
6.1 --- a/src/Tools/isac/Specify/specify-step.sml Thu Dec 07 11:54:42 2023 +0100
6.2 +++ b/src/Tools/isac/Specify/specify-step.sml Thu Dec 07 16:14:32 2023 +0100
6.3 @@ -51,7 +51,7 @@
6.4 | _ => raise ERROR "Specify_Step.check Model_Problem: uncovered case Ctree.get_obj"
6.5 val {model = model_patt, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
6.6 val pbl = I_Model.init_POS ctxt o_model model_patt
6.7 - in Applicable.Yes (Tactic.Model_Problem' (pI', I_Model.TEST_to_OLD pbl, [])) end
6.8 + in Applicable.Yes (Tactic.Model_Problem' (pI', pbl, [])) end
6.9 | check (Tactic.Refine_Problem pI) (pt, (p, _)) =
6.10 let
6.11 val (dI, dI', itms, ctxt) = case Ctree.get_obj I pt p of
6.12 @@ -63,11 +63,11 @@
6.13 case Refine.problem (ThyC.get_theory ctxt thy) pI itms of
6.14 NONE => Applicable.No
6.15 (Tactic.input_to_string ctxt (Tactic.Refine_Problem pI) ^ " not applicable")
6.16 - | SOME (rf as (pI', _)) =>
6.17 + | SOME (pI', (i_model, prec)) =>
6.18 if pI' = pI
6.19 then Applicable.No
6.20 (Tactic.input_to_string ctxt (Tactic.Refine_Problem pI) ^ " not applicable")
6.21 - else Applicable.Yes (Tactic.Refine_Problem' rf)
6.22 + else Applicable.Yes (Tactic.Refine_Problem' (pI', (I_Model.OLD_to_POS i_model, prec)))
6.23 end
6.24 | check (Tactic.Refine_Tacitly pI) (pt, (p, _)) =
6.25 let
6.26 @@ -85,7 +85,7 @@
6.27 let
6.28 val (o_model, _, i_model) = complete_for mID (ctree, pos)
6.29 in
6.30 - Applicable.Yes (Tactic.Specify_Method' (mID, o_model, I_Model.TEST_to_OLD i_model))
6.31 + Applicable.Yes (Tactic.Specify_Method' (mID, o_model, i_model))
6.32 end
6.33 | check (Tactic.Specify_Problem pID) (pt, pos as (p, _)) =
6.34 let
6.35 @@ -99,7 +99,7 @@
6.36 else M_Match.by_i_models ctxt oris
6.37 (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS meth) (model, where_, where_rls)
6.38 in
6.39 - Applicable.Yes (Tactic.Specify_Problem' (pID, (check, (I_Model.TEST_to_OLD i_model, preconds))))
6.40 + Applicable.Yes (Tactic.Specify_Problem' (pID, (check, (i_model, preconds))))
6.41 end
6.42 | check (Tactic.Specify_Theory dI)_ = Applicable.Yes (Tactic.Specify_Theory' dI)
6.43 | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable"
6.44 @@ -114,35 +114,35 @@
6.45 (* exceed line length, because result type will change *)
6.46 fun add (Tactic.Model_Problem' (_, itms, met)) (_, ctxt) (pt, pos as (p, _)) =
6.47 let
6.48 - val pt = Ctree.update_pbl pt p itms
6.49 - val pt = Ctree.update_met pt p met
6.50 + val pt = Ctree.update_pbl pt p (I_Model.TEST_to_OLD itms)
6.51 + val pt = Ctree.update_met pt p (I_Model.TEST_to_OLD met)
6.52 in
6.53 (pos, [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
6.54 end
6.55 | add (Tactic.Add_Given' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) =
6.56 (pos, [], Test_Out.PpcKF (Test_Out.Upblmet,P_Model.from (Proof_Context.theory_of ctxt) [][]),
6.57 case p_ of
6.58 - Pos.Pbl => Ctree.update_pbl pt p itmlist
6.59 - | Pos.Met => Ctree.update_met pt p itmlist
6.60 + Pos.Pbl => Ctree.update_pbl pt p (I_Model.TEST_to_OLD itmlist)
6.61 + | Pos.Met => Ctree.update_met pt p (I_Model.TEST_to_OLD itmlist)
6.62 | _ => raise ERROR ("uncovered case " ^ Pos.pos_2str p_))
6.63 | add (Tactic.Add_Find' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) =
6.64 (pos, [], (Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] [])),
6.65 case p_ of
6.66 - Pos.Pbl => Ctree.update_pbl pt p itmlist
6.67 - | Pos.Met => Ctree.update_met pt p itmlist
6.68 + Pos.Pbl => Ctree.update_pbl pt p (I_Model.TEST_to_OLD itmlist)
6.69 + | Pos.Met => Ctree.update_met pt p (I_Model.TEST_to_OLD itmlist)
6.70 | _ => raise ERROR ("uncovered case " ^ Pos.pos_2str p_))
6.71 | add (Tactic.Add_Relation' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) =
6.72 (pos, [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []),
6.73 case p_ of
6.74 - Pos.Pbl => Ctree.update_pbl pt p itmlist
6.75 - | Pos.Met => Ctree.update_met pt p itmlist
6.76 + Pos.Pbl => Ctree.update_pbl pt p (I_Model.TEST_to_OLD itmlist)
6.77 + | Pos.Met => Ctree.update_met pt p (I_Model.TEST_to_OLD itmlist)
6.78 | _ => raise ERROR ("uncovered case " ^ Pos.pos_2str p_))
6.79 | add (Tactic.Specify_Theory' domID) (_, ctxt) (pt, pos as (p,_)) =
6.80 (pos, [] , Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []),
6.81 Ctree.update_domID pt p domID)
6.82 | add (Tactic.Specify_Problem' (pI, (_, (itms, _)))) (_, ctxt) (pt, (p, _)) =
6.83 let
6.84 - val pt = Ctree.update_pbl pt p itms
6.85 + val pt = Ctree.update_pbl pt p (I_Model.TEST_to_OLD itms)
6.86 val pt = Ctree.update_pblID pt p pI
6.87 in
6.88 ((p, Pos.Pbl), [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
6.89 @@ -150,14 +150,14 @@
6.90 | add (Tactic.Specify_Method' (mID, oris, itms)) (_, ctxt) (pt, (p, _)) =
6.91 let
6.92 val pt = Ctree.update_oris pt p oris
6.93 - val pt = Ctree.update_met pt p itms
6.94 + val pt = Ctree.update_met pt p (I_Model.TEST_to_OLD itms)
6.95 val pt = Ctree.update_metID pt p mID
6.96 in
6.97 ((p, Pos.Met), [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
6.98 end
6.99 | add (Tactic.Refine_Tacitly' (_, pIre, domID, metID, pbl)) (_, ctxt) (pt, pos as (p, _)) =
6.100 let
6.101 - val pt = Ctree.update_pbl pt p pbl
6.102 + val pt = Ctree.update_pbl pt p (I_Model.TEST_to_OLD pbl)
6.103 val pt = Ctree.update_orispec pt p (domID, pIre, metID)
6.104 in
6.105 (pos, [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
7.1 --- a/src/Tools/isac/Specify/specify.sml Thu Dec 07 11:54:42 2023 +0100
7.2 +++ b/src/Tools/isac/Specify/specify.sml Thu Dec 07 16:14:32 2023 +0100
7.3 @@ -157,7 +157,7 @@
7.4 I_Model.Add i_single => (*..union old input *)
7.5 let
7.6 val i_model' = I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model
7.7 - val tac' = I_Model.make_tactic m_field (ct, I_Model.TEST_to_OLD i_model')
7.8 + val tac' = I_Model.make_tactic m_field (ct, i_model')
7.9 val (_, _, _, pt') = Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, pos)
7.10 in
7.11 ("ok", ([(Tactic.input_from_T ctxt tac', tac', (pos, (Istate_Def.Uistate, ctxt)))],
8.1 --- a/src/Tools/isac/Specify/step-specify.sml Thu Dec 07 11:54:42 2023 +0100
8.2 +++ b/src/Tools/isac/Specify/step-specify.sml Thu Dec 07 16:14:32 2023 +0100
8.3 @@ -33,7 +33,7 @@
8.4 val (pbl, met) = case cas of
8.5 NONE => (pbl, [])
8.6 | _ => I_Model.s_make_complete ctxt oris (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS meth) (pI, mI)
8.7 - val tac_ = Tactic.Model_Problem' (pI, I_Model.TEST_to_OLD pbl, I_Model.TEST_to_OLD met)
8.8 + val tac_ = Tactic.Model_Problem' (pI, pbl, met)
8.9 val (pos,c,_,pt) = Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, pos)
8.10 in
8.11 ("ok",([(tac, tac_, (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos)))
8.12 @@ -74,12 +74,13 @@
8.13 in
8.14 case Refine.problem (ThyC.get_theory ctxt thy) pI probl of
8.15 NONE => ("failure", ([], [], ptp))
8.16 - | SOME rfd =>
8.17 + | SOME (pI, (i_model, prec)) =>
8.18 let
8.19 - val (pos,c,_,pt) = Specify_Step.add (Tactic.Refine_Problem' rfd) (Istate_Def.Uistate, ctxt) (pt, pos)
8.20 + val (pos,c,_,pt) = Specify_Step.add (Tactic.Refine_Problem' (pI, (I_Model.OLD_to_POS i_model, prec)) )
8.21 + (Istate_Def.Uistate, ctxt) (pt, pos)
8.22 in
8.23 - ("ok", ([(Tactic.Refine_Problem pI, Tactic.Refine_Problem' rfd,
8.24 - (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos)))
8.25 + ("ok", ([(Tactic.Refine_Problem pI, Tactic.Refine_Problem' (pI, (I_Model.OLD_to_POS i_model, prec)),
8.26 + (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt, pos)))
8.27 end
8.28 end
8.29 | by_tactic_input (Tactic.Specify_Problem pI) (pt, pos as (p, _)) =
8.30 @@ -95,20 +96,20 @@
8.31 else M_Match.by_i_models ctxt oris
8.32 (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS meth) (model, where_, where_rls)
8.33 val (c, pt) =
8.34 - case Specify_Step.add (Tactic.Specify_Problem' (pI, (check, (I_Model.TEST_to_OLD i_model, preconds)))) (Istate_Def.Uistate, ctxt) (pt, pos) of
8.35 + case Specify_Step.add (Tactic.Specify_Problem' (pI, (check, (i_model, preconds)))) (Istate_Def.Uistate, ctxt) (pt, pos) of
8.36 ((_, Pbl), c, _, pt) => (c, pt)
8.37 | _ => raise ERROR ""
8.38 in
8.39 - ("ok", ([(Tactic.Specify_Problem pI, Tactic.Specify_Problem' (pI, (check, (I_Model.TEST_to_OLD i_model, preconds))),
8.40 + ("ok", ([(Tactic.Specify_Problem pI, Tactic.Specify_Problem' (pI, (check, ( i_model, preconds))),
8.41 (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt, pos)))
8.42 end
8.43 | by_tactic_input (Tactic.Specify_Method id) (pt, pos) =
8.44 let
8.45 val (o_model, ctxt, i_model) = Specify_Step.complete_for id (pt, pos)
8.46 - val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (id, o_model, I_Model.TEST_to_OLD i_model))
8.47 + val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (id, o_model, i_model))
8.48 (Istate_Def.Uistate, ctxt) (pt, pos)
8.49 in
8.50 - ("ok", ([(Tactic.Specify_Method id, Tactic.Specify_Method' (id, o_model, I_Model.TEST_to_OLD i_model),
8.51 + ("ok", ([(Tactic.Specify_Method id, Tactic.Specify_Method' (id, o_model, i_model),
8.52 (pos, (Istate_Def.Uistate, ContextC.empty)))], [], (pt, pos)))
8.53 end
8.54 | by_tactic_input (Tactic.Specify_Theory dI) (pt, pos as (_, Pbl)) =
8.55 @@ -184,7 +185,7 @@
8.56 | by_tactic (Tactic.Specify_Method' (id, _, _)) (pt, pos) =
8.57 let
8.58 val (o_model, ctxt, i_model) = Specify_Step.complete_for id (pt, pos)
8.59 - val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (id, o_model, I_Model.TEST_to_OLD i_model))
8.60 + val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (id, o_model, i_model))
8.61 (Istate_Def.Uistate, ctxt) (pt, pos)
8.62 in
8.63 ("ok", ([], [], (pt, pos)))
9.1 --- a/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Thu Dec 07 11:54:42 2023 +0100
9.2 +++ b/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Thu Dec 07 16:14:32 2023 +0100
9.3 @@ -123,7 +123,7 @@
9.4 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_POS Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_POS AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_POS Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_POS SideConditions [] [__=__, __=__], Position.T))]"
9.5 = i_model' |> I_Model.to_string_POS ctxt
9.6
9.7 - val tac' = I_Model.make_tactic m_field (ct, I_Model.TEST_to_OLD i_model')
9.8 + val tac' = I_Model.make_tactic m_field (ct, i_model')
9.9 val (_, _, _, pt') = Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, pos)
9.10 val return_by_Add_step =
9.11 ("ok", ([(Tactic.input_from_T ctxt tac', tac', (pos, (Istate_Def.Uistate, ctxt)))],