equal
deleted
inserted
replaced
7 sig |
7 sig |
8 datatype auto = CompleteCalc | CompleteCalcHead | CompleteModel | CompleteSubpbl |
8 datatype auto = CompleteCalc | CompleteCalcHead | CompleteModel | CompleteSubpbl |
9 | CompleteToSubpbl | Steps of int |
9 | CompleteToSubpbl | Steps of int |
10 val autoord : auto -> int |
10 val autoord : auto -> int |
11 |
11 |
12 val all_solve : auto -> Ctree.pos' list -> Calc.T -> |
12 val all_solve : auto -> Pos.pos' list -> Calc.T -> |
13 string * Ctree.pos' list * (Ctree.ctree * (int list * Ctree.pos_)) |
13 string * Pos.pos' list * (Ctree.ctree * (int list * Pos.pos_)) |
14 val complete_solve : |
14 val complete_solve : |
15 auto -> Ctree.pos' list -> Calc.T -> string * Ctree.pos' list * Calc.T |
15 auto -> Pos.pos' list -> Calc.T -> string * Pos.pos' list * Calc.T |
16 |
16 |
17 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
17 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
18 (*NONE*) |
18 (*NONE*) |
19 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
19 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
20 (*NONE*) |
20 (*NONE*) |
85 | (_, (_, c', ptp')) => complete_solve auto (c @ c') ptp' |
85 | (_, (_, c', ptp')) => complete_solve auto (c @ c') ptp' |
86 and all_solve auto c (ptp as (pt, pos as (p,_)): ctree * pos') = |
86 and all_solve auto c (ptp as (pt, pos as (p,_)): ctree * pos') = |
87 let |
87 let |
88 val (_, _, mI) = get_obj g_spec pt p |
88 val (_, _, mI) = get_obj g_spec pt p |
89 val ctxt = get_ctxt pt pos |
89 val ctxt = get_ctxt pt pos |
90 val (_, (_, c', ptp)) = LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ctxt)) (Istate.e_istate, ctxt) ptp |
90 val (_, (_, c', ptp)) = LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ctxt)) (Istate.empty, ctxt) ptp |
91 in |
91 in |
92 complete_solve auto (c @ c') ptp |
92 complete_solve auto (c @ c') ptp |
93 end; |
93 end; |
94 |
94 |
95 end |
95 end |