1.1 --- a/src/Tools/isac/Interpret/error-fill-pattern.sml Thu Apr 23 12:34:54 2020 +0200
1.2 +++ b/src/Tools/isac/Interpret/error-fill-pattern.sml Thu Apr 23 15:48:31 2020 +0200
1.3 @@ -17,14 +17,9 @@
1.4 (Error_Fill_Def.fillpatID * term * thm * Selem.subs option) list
1.5 val fetchErrorpatterns : Tactic.input -> Error_Fill_Def.errpatID list
1.6 val is_exactly_equal : Calc.T -> string -> string * Tactic.input
1.7 -
1.8 -(*/------- to LItool -------\*)
1.9 - val mk_tacis: Rewrite_Ord.rew_ord' * 'a -> Rule_Set.T -> term * Rule.rule * (term * term list) ->
1.10 - Tactic.input * Tactic.T * (Pos.pos' * (Istate.T * Proof.context))
1.11 val check_for : term * term -> term * (term * term) list ->
1.12 (Error_Fill_Def.errpatID * term list * 'a list) list * Rule_Set.T ->
1.13 Error_Fill_Def.errpatID option
1.14 -(*\------- to LItool -------/*)
1.15
1.16 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.17 (* NONE *)
1.18 @@ -44,18 +39,6 @@
1.19
1.20 type errpatID = Rule_Def.errpatID
1.21
1.22 -fun mk_tacis ro erls (t, r as Rule.Thm (id, thm), (t', a)) =
1.23 - (Tactic.Rewrite (id, thm),
1.24 - Tactic.Rewrite' ("Isac_Knowledge", fst ro, erls, false, ThmC.from_rule r, t, (t', a)),
1.25 - (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate.Uistate, ContextC.empty)))
1.26 - | mk_tacis _ _ (t, r as Rule.Rls_ rls, (t', a)) =
1.27 - (Tactic.Rewrite_Set (Rule_Set.id_from_rule r),
1.28 - Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)),
1.29 - (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate.Uistate, ContextC.empty)))
1.30 - | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ Rule.to_string r ^ " at " ^ UnparseC.term t)
1.31 -
1.32 -
1.33 -(*** handle an error pattern ***)
1.34
1.35 (* check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls *)
1.36 fun check_err_patt (res, inf) subst (errpatID, pat) rls =
1.37 @@ -76,8 +59,10 @@
1.38 else NONE
1.39 end;
1.40
1.41 -(* check if (agreed result, input formula) matches SOME error pattern modulo simplifier rls;
1.42 - (prog, env) for retrieval of casual substitution for bdv in the pattern. *)
1.43 +(*
1.44 + check if (agreed result, input formula) matches SOME error pattern modulo simplifier rls;
1.45 + (prog, env) for retrieval of casual substitution for bdv in the pattern.
1.46 +*)
1.47 fun check_for (res, inf) (prog, env) (errpats, rls) =
1.48 let
1.49 val (_, subst) = Rtools.get_bdv_subst prog env
2.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Apr 23 12:34:54 2020 +0200
2.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Apr 23 15:48:31 2020 +0200
2.3 @@ -46,7 +46,7 @@
2.4 val check_tac: Calc.T * Proof.context -> Istate.pstate -> term * term option -> expr_val
2.5 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.6 val check_Let_up: Istate.pstate -> term -> term * term
2.7 - val compare_step: Generate.taci list * Pos.pos' list * (Calc.T) -> term -> string * Chead.calcstate'
2.8 + val compare_step: State_Steps.T * Pos.pos' list * Calc.T -> term -> string * Chead.calcstate'
2.9
2.10 val scan_dn1: (Calc.T * Proof.context * Tactic.T) -> Istate.pstate -> term -> expr_val1
2.11 val scan_up1: term * (Calc.T * Proof.context * Tactic.T) -> Istate.pstate -> term -> expr_val1;
2.12 @@ -627,7 +627,7 @@
2.13 if found
2.14 then
2.15 let
2.16 - val tacis' = map (Error_Fill_Pattern.mk_tacis rew_ord erls) der;
2.17 + val tacis' = map (State_Steps.make_single rew_ord erls) der;
2.18 val (c', ptp) = Generate.embed_deriv tacis' ptp;
2.19 in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end
2.20 else
3.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy Thu Apr 23 12:34:54 2020 +0200
3.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy Thu Apr 23 15:48:31 2020 +0200
3.3 @@ -25,6 +25,7 @@
3.4 ML_file "ctree-access.sml"
3.5 ML_file "ctree-navi.sml"
3.6 ML_file ctree.sml
3.7 + ML_file "state-steps.sml"
3.8 ML_file calculation.sml
3.9
3.10 ML \<open>
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/Tools/isac/MathEngBasic/state-steps.sml Thu Apr 23 15:48:31 2020 +0200
4.3 @@ -0,0 +1,75 @@
4.4 +(* Title: TODO/state-step.sml
4.5 + Author: Walther Neuper
4.6 + (c) due to copyright terms
4.7 +
4.8 +Deprecated; the idea was to hold steps complete such, that they can be replayed.
4.9 +*)
4.10 +
4.11 +signature STATE_STEPS =
4.12 +sig
4.13 + type single
4.14 + val single_empty : single
4.15 + type T
4.16 + val to_string : T -> string
4.17 + val result : single -> (term * term list)
4.18 + val make_single: Rewrite_Ord.rew_ord' * 'a -> Rule_Set.T -> term * Rule.rule * (term * term list) ->
4.19 + Tactic.input * Tactic.T * (Pos.pos' * (Istate_Def.T * Proof.context))
4.20 + val insert_pos : Pos.pos -> T -> T
4.21 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.22 + (* NONE *)
4.23 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.24 + (* NONE *)
4.25 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
4.26 +end
4.27 +
4.28 +(**)
4.29 +structure State_Steps(**): STATE_STEPS(**) =
4.30 +struct
4.31 +(**)
4.32 +
4.33 +(*/------- to State_Steps from Generate -------\*)
4.34 +(* a single holds alle information required to build a node in the calc-tree;
4.35 + a single is assumed to be used efficiently such that the calc-tree
4.36 + resulting from applying a single need not be stored separately;
4.37 + see "type calcstate" *)
4.38 +(*TODO.WN0504 redesign ??? or redesign generate ?? see "fun generate"
4.39 + TODO.WN0512 ? redesign this _list_:
4.40 + # only used for [Apply_Method + (Take or Subproblem)], i.e. for initacs
4.41 + # the latter problem may be resolved automatically if "fun autocalc" is
4.42 + not any more used for the specify-phase and for changing the phases*)
4.43 +type single =
4.44 + (Tactic.input * (* for comparison with input tac *)
4.45 + Tactic.T * (* for ctree generation *)
4.46 + (Pos.pos' * (* after applying tac_, for ctree generation *)
4.47 + (Istate_Def.T * Proof.context))) (* after applying tac_, for ctree generation *)
4.48 +val single_empty = (Tactic.Empty_Tac, Tactic.Empty_Tac_, (Pos.e_pos', (Istate_Def.empty, ContextC.empty))): single
4.49 +fun taci2str ((tac, tac_, (pos', (istate, _))):single) =
4.50 + "( " ^ Tactic.input_to_string tac ^ ", " ^ Tactic.string_of tac_ ^ ", ( " ^ Pos.pos'2str pos' ^ ", " ^
4.51 + Istate_Def.string_of istate ^ " ))"
4.52 +
4.53 +type T = single list;
4.54 +
4.55 +fun to_string tacis = (strs2str o (map (linefeed o taci2str))) tacis
4.56 +fun result (_, Tactic.Rewrite' (_, _, _, _, _, _,(res, asm)), _) = (res, asm)
4.57 + | result (_, Tactic.Rewrite_Set' (_, _, _, _, (res, asm)), _) = (res, asm)
4.58 + | result (_, tac_, _) = error ("result: called with" ^ Tactic.string_of tac_)
4.59 +(*\------- to State_Steps from Generate -------/*)
4.60 +(*/------- to State_Steps from Error_Pattern -------\*)
4.61 +fun make_single ro erls (t, r as Rule.Thm (id, thm), (t', a)) =
4.62 + (Tactic.Rewrite (id, thm),
4.63 + Tactic.Rewrite' ("Isac_Knowledge", fst ro, erls, false, ThmC.from_rule r, t, (t', a)),
4.64 + (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty)))
4.65 + | make_single _ _ (t, r as Rule.Rls_ rls, (t', a)) =
4.66 + (Tactic.Rewrite_Set (Rule_Set.id_from_rule r),
4.67 + Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)),
4.68 + (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty)))
4.69 + | make_single _ _ (t, r, _) = error ("make_single: not impl. for " ^ Rule.to_string r ^ " at " ^ UnparseC.term t)
4.70 +(*\------- to State_Steps from Error_Pattern -------/*)
4.71 +
4.72 +(* update pos in tacis for embedding by generate *)
4.73 +fun insert_pos (_: Pos.pos) [] = []
4.74 + | insert_pos (p: Pos.pos) (((tac, tac_, (_, ist)): single) :: tacis) =
4.75 + ((tac, tac_, ((p, Pos.Res), ist)): single) :: (insert_pos (Pos.lev_on p) tacis)
4.76 +
4.77 +(**)end(**)
4.78 +
5.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Thu Apr 23 12:34:54 2020 +0200
5.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Thu Apr 23 15:48:31 2020 +0200
5.3 @@ -7,8 +7,8 @@
5.4
5.5 signature MATH_ENGINE =
5.6 sig
5.7 - val autocalc : Pos.pos' list -> Pos.pos' -> (Calc.T) * Generate.taci list ->
5.8 - Solve.auto -> string * Pos.pos' list * (Calc.T)
5.9 + val autocalc : Pos.pos' list -> Pos.pos' -> Calc.T * State_Steps.T ->
5.10 + Solve.auto -> string * Pos.pos' list * Calc.T
5.11
5.12 val initcontext_met : Ctree.ctree -> Pos.pos' -> bool * string list * Program.T * Model.itm list * (bool * term) list
5.13 val initcontext_pbl : Ctree.ctree -> Pos.pos' -> bool * string list * term * Model.itm list * (bool * term) list
6.1 --- a/src/Tools/isac/Specify/calchead.sml Thu Apr 23 12:34:54 2020 +0200
6.2 +++ b/src/Tools/isac/Specify/calchead.sml Thu Apr 23 15:48:31 2020 +0200
6.3 @@ -108,7 +108,7 @@
6.4 val vals_of_oris : Model.ori list -> term list
6.5 val specify_additem: string -> TermC.as_string -> Calc.T -> string * calcstate'
6.6 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
6.7 - val e_calcstate : Calc.T * Generate.taci list
6.8 + val e_calcstate : Calc.T * State_Steps.T
6.9 val e_calcstate' : calcstate'
6.10 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
6.11 val posterms2str : (Pos.pos' * term * 'a) list -> string
6.12 @@ -161,9 +161,9 @@
6.13 *)
6.14 type calcstate =
6.15 (ctree * pos') * (* the calc-state to which the tacis could be applied *)
6.16 - (Generate.taci list) (* ev. several (hidden) steps;
6.17 + State_Steps.T (* ev. several (hidden) steps;
6.18 in REVERSE order: first tac_ to apply is last_elem *)
6.19 -val e_calcstate = ((EmptyPtree, e_pos'), [Generate.e_taci]);
6.20 +val e_calcstate = ((EmptyPtree, e_pos'), [State_Steps.single_empty]);
6.21
6.22 (*the state used during one calculation within the mathengine; it contains
6.23 a list of [tac,istate](="tacis") which generated the the calc-state;
6.24 @@ -175,11 +175,11 @@
6.25 because the tacis hold enought information for efficiently rebuilding
6.26 this state just by "fun generate ".*)
6.27 type calcstate' =
6.28 - Generate.taci list * (* cas. several (hidden) steps;
6.29 + State_Steps.T * (* cas. several (hidden) steps;
6.30 in REVERSE order: first tac_ to apply is last_elem *)
6.31 pos' list * (* a "continuous" sequence of pos', deleted by application of taci list *)
6.32 (ctree * pos') (* the calc-state resulting from the application of tacis *)
6.33 -val e_calcstate' = ([Generate.e_taci], [e_pos'], (EmptyPtree, e_pos')) : calcstate';
6.34 +val e_calcstate' = ([State_Steps.single_empty], [e_pos'], (EmptyPtree, e_pos')) : calcstate';
6.35
6.36 (* is the calchead complete ? *)
6.37 fun ocalhd_complete its pre (dI, pI, mI) =
7.1 --- a/src/Tools/isac/Specify/generate.sml Thu Apr 23 12:34:54 2020 +0200
7.2 +++ b/src/Tools/isac/Specify/generate.sml Thu Apr 23 15:48:31 2020 +0200
7.3 @@ -5,8 +5,6 @@
7.4
7.5 signature GENERATE_CALC_TREE =
7.6 sig
7.7 - type taci
7.8 - val e_taci : taci
7.9 datatype pblmet = Method of Method.id | Problem of Problem.id | Upblmet
7.10 datatype mout =
7.11 EmptyMout
7.12 @@ -19,27 +17,24 @@
7.13 val init_istate : Tactic.input -> term -> Istate_Def.T
7.14 val init_pbl : (string * (term * 'a)) list -> Model.itm list
7.15 val init_pbl' : (string * (term * term)) list -> Model.itm list
7.16 - val embed_deriv : taci list -> Calc.T -> Pos.pos' list * (Calc.T) (* for inform.sml *)
7.17 - val generate_hard : (* for solve.sml *)
7.18 + val embed_deriv : State_Steps.T -> Calc.T -> Pos.pos' list * Calc.T
7.19 + val generate_hard :
7.20 theory -> Tactic.T -> Pos.pos' -> Ctree.ctree -> Pos.pos' * Pos.pos' list * mout * Ctree.ctree
7.21 val generate : (Tactic.input * Tactic.T * (Pos.pos' * (Istate_Def.T * Proof.context))) list ->
7.22 - Ctree.ctree * Pos.pos' list * Pos.pos' -> Ctree.ctree * Pos.pos' list * Pos.pos' (* for mathengine.sml *)
7.23 + Ctree.ctree * Pos.pos' list * Pos.pos' -> Ctree.ctree * Pos.pos' list * Pos.pos'
7.24 val generate_inconsistent_rew : Selem.subs option * ThmC.T -> term -> Istate_Def.T * Proof.context ->
7.25 - Pos.pos' -> Ctree.ctree -> Calc.T (* for interface.sml *)
7.26 + Pos.pos' -> Ctree.ctree -> Calc.T
7.27 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
7.28 - val tacis2str : taci list -> string
7.29 val mout2str : mout -> string
7.30 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
7.31 - val res_from_taci : taci -> (term * term list)
7.32 - val insert_pos : Pos.pos -> taci list -> taci list
7.33 + (* NONE *)
7.34 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
7.35 -
7.36 -(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
7.37 - (* NONE *)
7.38 end
7.39
7.40 +(**)
7.41 structure Generate(**): GENERATE_CALC_TREE(**) =
7.42 struct
7.43 +(**)
7.44 open Ctree
7.45 open Pos
7.46
7.47 @@ -65,25 +60,6 @@
7.48 end
7.49 | init_istate tac _ = error ("init_istate: uncovered definition for " ^ Tactic.input_to_string tac)
7.50
7.51 -(* a taci holds alle information required to build a node in the calc-tree;
7.52 - a taci is assumed to be used efficiently such that the calc-tree
7.53 - resulting from applying a taci need not be stored separately;
7.54 - see "type calcstate" *)
7.55 -(*TODO.WN0504 redesign ??? or redesign generate ?? see "fun generate"
7.56 - TODO.WN0512 ? redesign this _list_:
7.57 - # only used for [Apply_Method + (Take or Subproblem)], i.e. for initacs
7.58 - # the latter problem may be resolved automatically if "fun autocalc" is
7.59 - not any more used for the specify-phase and for changing the phases*)
7.60 -type taci =
7.61 - (Tactic.input * (* for comparison with input tac *)
7.62 - Tactic.T * (* for ctree generation *)
7.63 - (pos' * (* after applying tac_, for ctree generation *)
7.64 - (Istate_Def.T * Proof.context))) (* after applying tac_, for ctree generation *)
7.65 -val e_taci = (Tactic.Empty_Tac, Tactic.Empty_Tac_, (e_pos', (Istate_Def.empty, ContextC.empty))): taci
7.66 -fun taci2str ((tac, tac_, (pos', (istate, _))):taci) =
7.67 - "( " ^ Tactic.input_to_string tac ^ ", " ^ Tactic.string_of tac_ ^ ", ( " ^ pos'2str pos' ^ ", " ^
7.68 - Istate_Def.string_of istate ^ " ))"
7.69 -fun tacis2str tacis = (strs2str o (map (linefeed o taci2str))) tacis
7.70
7.71 datatype pblmet = (*%^%*)
7.72 Upblmet (*undefined*)
7.73 @@ -366,7 +342,7 @@
7.74 end
7.75
7.76 (* tacis are in reverse order from do_next/specify_: last = fst to insert *)
7.77 -fun generate ([]: taci list) ptp = ptp
7.78 +fun generate ([]: State_Steps.T) ptp = ptp
7.79 | generate tacis (pt, c, _: pos'(*!dropped!WN0504redesign generate/tacis?*)) =
7.80 let
7.81 val (tacis', (_, tac_, (p, is))) = split_last tacis
7.82 @@ -375,29 +351,20 @@
7.83 generate tacis' (pt', c@c', p')
7.84 end
7.85
7.86 -(* update pos in tacis for embedding by generate *)
7.87 -fun insert_pos (_: pos) [] = []
7.88 - | insert_pos (p: pos) (((tac, tac_, (_, ist)): taci) :: tacis) =
7.89 - ((tac, tac_, ((p, Res), ist)): taci) :: (insert_pos (lev_on p) tacis)
7.90 -
7.91 -fun res_from_taci (_, Tactic.Rewrite' (_, _, _, _, _, _,(res, asm)), _) = (res, asm)
7.92 - | res_from_taci (_, Tactic.Rewrite_Set' (_, _, _, _, (res, asm)), _) = (res, asm)
7.93 - | res_from_taci (_, tac_, _) = error ("res_from_taci: called with" ^ Tactic.string_of tac_)
7.94 -
7.95 (* embed the tacis created by a '_deriv'ation; sys.form <> input.form
7.96 tacis are in order, thus are reverted for generate *)
7.97 fun embed_deriv tacis (pt, pos as (p, Frm)) =
7.98 (*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj FIXME?0402
7.99 and transfer the istate (from _after_ compare_deriv) from Frm to Res*)
7.100 let
7.101 - val (res, asm) = (res_from_taci o last_elem) tacis
7.102 + val (res, asm) = (State_Steps.result o last_elem) tacis
7.103 val (ist, ctxt) = case get_obj g_loc pt p of
7.104 (SOME (ist, ctxt), _) => (ist, ctxt)
7.105 | (NONE, _) => error "embed_deriv Frm: uncovered case get_obj"
7.106 val form = get_obj g_form pt p
7.107 (*val p = lev_on p; ---------------only difference to (..,Res) below*)
7.108 val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' form, (pos, (Istate_Def.Uistate, ctxt))) ::
7.109 - (insert_pos ((lev_on o lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
7.110 + (State_Steps.insert_pos ((lev_on o lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
7.111 (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))]
7.112 val {nrls, ...} = Specify.get_met (get_obj g_metID pt (par_pblobj pt p))
7.113 val (pt, c, pos as (p, _)) = generate (rev tacis) (pt, [], (p, Res))
7.114 @@ -407,14 +374,14 @@
7.115 | embed_deriv tacis (pt, (p, Res)) =
7.116 (*inform at Res: append a Transitive-PrfObj FIXME?0402 other branch-types ?
7.117 and transfer the istate (from _after_ compare_deriv) from Res to new Res*)
7.118 - let val (res, asm) = (res_from_taci o last_elem) tacis
7.119 + let val (res, asm) = (State_Steps.result o last_elem) tacis
7.120 val (ist, ctxt) = case get_obj g_loc pt p of
7.121 (_, SOME (ist, ctxt)) => (ist, ctxt)
7.122 | (_, NONE) => error "embed_deriv Frm: uncovered case get_obj"
7.123 val (f, _) = get_obj g_result pt p
7.124 val p = lev_on p(*---------------only difference to (..,Frm) above*);
7.125 val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Frm), (Istate_Def.Uistate, ctxt))) ::
7.126 - (insert_pos ((lev_on o lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
7.127 + (State_Steps.insert_pos ((lev_on o lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
7.128 (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))];
7.129 val {nrls, ...} = Specify.get_met (get_obj g_metID pt (par_pblobj pt p))
7.130 val (pt, c, pos as (p, _)) = generate (rev tacis) (pt, [], (p, Res))
8.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Thu Apr 23 12:34:54 2020 +0200
8.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Thu Apr 23 15:48:31 2020 +0200
8.3 @@ -179,7 +179,7 @@
8.4 Rewrite_Set_Inst' _, (pos', (istate, ctxt))) ] , _, cstate)) = xxxxx_x;
8.5
8.6 (*//******************* Step.by_tactic returns tac_ + istate + cstate *****************************\\*)
8.7 -Step.by_tactic : Tactic.input -> state -> string * (taci list * pos' list * state);
8.8 +Step.by_tactic : Tactic.input -> state -> string * (State_Steps.T * pos' list * state);
8.9 if Istate.string_of istate
8.10 = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], empty, SOME e_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, true, true)"
8.11 then () else error "from Step.by_tactic return --- changed 1";
9.1 --- a/test/Tools/isac/OLDTESTS/tacis.sml Thu Apr 23 12:34:54 2020 +0200
9.2 +++ b/test/Tools/isac/OLDTESTS/tacis.sml Thu Apr 23 15:48:31 2020 +0200
9.3 @@ -48,7 +48,7 @@
9.4 fetchProposedTactic 1 (*'Apply_Method Test solve_linear' in tacis*);
9.5 (* there was the only error ^^^^^^^^^ in step/begin_end_prog ..Apply_Method..
9.6 val (str', (tacis', (pt',p'))) = Step.do_next ip (ptp, tacis);
9.7 - writeln (tacis2str tacis');
9.8 + writeln (State_Steps.to_string tacis');
9.9 ######################################################################*)
9.10 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*-1 + x = 0*);
9.11