47 val SOME _ = (*case*) pIopt (*of*); |
47 val SOME _ = (*case*) pIopt (*of*); |
48 (*if*) member op = [Pos.Pbl, Pos.Met] p_ |
48 (*if*) member op = [Pos.Pbl, Pos.Met] p_ |
49 andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p)) (*then*); |
49 andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p)) (*then*); |
50 |
50 |
51 val ("dummy", ([(Specify_Theory "Integrate", _, _)], _, _)) = |
51 val ("dummy", ([(Specify_Theory "Integrate", _, _)], _, _)) = |
52 nxt_specify_ (pt, ip); |
52 Step.specify_do_next (pt, ip); |
53 "~~~~~ fun nxt_specify_ , args:"; val ((ptp as (pt, (p, p_)))) = (pt, ip); |
53 "~~~~~ fun nxt_specify_ , args:"; val ((ptp as (pt, (p, p_)))) = (pt, ip); |
54 val (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI) = |
54 val (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI) = |
55 (*isa<>REP ^^*) |
55 (*isa<>REP ^^*) |
56 case Ctree.get_obj I pt p of |
56 case Ctree.get_obj I pt p of |
57 pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _), |
57 pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _), |
79 (Pbl, Tactic.Specify_Theory dI') (*return from nxt_spec*); |
79 (Pbl, Tactic.Specify_Theory dI') (*return from nxt_spec*); |
80 "~~~~~ from fun nxt_spec\<longrightarrow>fun nxt_specify_, return:"; val (_, tac) |
80 "~~~~~ from fun nxt_spec\<longrightarrow>fun nxt_specify_, return:"; val (_, tac) |
81 = (Pbl, Tactic.Specify_Theory dI'); |
81 = (Pbl, Tactic.Specify_Theory dI'); |
82 val _ = (*case*) tac (*of*); |
82 val _ = (*case*) tac (*of*); |
83 |
83 |
84 ("dummy", Chead.nxt_specif tac ptp) (*return from nxt_specify_*); |
84 ("dummy", Step_Specify.by_tactic tac ptp) (*return from nxt_specify_*); |
85 "~~~~~ from fun nxt_specify_\<longrightarrow>fun Math_Engine.do_next\<longrightarrow>fun autocalc, return:"; val (str, (_, c', ptp)) |
85 "~~~~~ from fun nxt_specify_\<longrightarrow>fun Math_Engine.do_next\<longrightarrow>fun autocalc, return:"; val (str, (_, c', ptp)) |
86 = ("dummy", Chead.nxt_specif tac ptp); |
86 = ("dummy", Step_Specify.by_tactic tac ptp); |
87 |
87 |
88 (str, c''''' @ c', ptp) (*return from autocalc*); |
88 (str, c''''' @ c', ptp) (*return from autocalc*); |
89 |
89 |
90 "----- step 2 ---";(*isa<>REP*) |
90 "----- step 2 ---";(*isa<>REP*) |
91 autoCalculate 1 (Steps 1); |
91 autoCalculate 1 (Steps 1); |