62 tacis; (*= []*) |
62 tacis; (*= []*) |
63 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*) |
63 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*) |
64 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); |
64 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); |
65 val thy' = get_obj g_domID pt (par_pblobj pt p); |
65 val thy' = get_obj g_domID pt (par_pblobj pt p); |
66 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; |
66 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; |
67 "~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ctree * pos'), (sc as Prog (h $ body)), |
67 "~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt,(p,_)):ctree * pos'), (sc as Prog (h $ body)), |
68 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is); |
68 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is); |
69 val ctxt = get_ctxt pt pos; |
69 val ctxt = get_ctxt pt pos; |
70 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}"; |
70 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}"; |
71 (*= the first part ^^^^^^^^^^ works now =======================================*) |
71 (*= the first part ^^^^^^^^^^ works now =======================================*) |
72 l = []; |
72 l = []; |