45 |
45 |
46 "~~~~~ and do_solve_step , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); |
46 "~~~~~ and do_solve_step , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); |
47 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*) |
47 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*) |
48 val thy' = get_obj g_domID pt (par_pblobj pt p); |
48 val thy' = get_obj g_domID pt (par_pblobj pt p); |
49 val (srls, (ist, ctxt), sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*) |
49 val (srls, (ist, ctxt), sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*) |
50 val End_Program (ist, tac) = determine_next_tactic sc (pt,pos) ist ctxt; |
50 val End_Program (ist, tac) = find_next_tactic sc (pt,pos) ist ctxt; |
51 |
51 |
52 (*+*);tac; (* = Check_Postcond' *) |
52 (*+*);tac; (* = Check_Postcond' *) |
53 |
53 |
54 "~~~~~ fun begin_end_prog , args:"; val ((Check_Postcond' (pI, (prog_res, _))), _, (pt, pos as (p,p_))) = |
54 "~~~~~ fun begin_end_prog , args:"; val ((Check_Postcond' (pI, (prog_res, _))), _, (pt, pos as (p,p_))) = |
55 (tac, (ist, ctxt), ptp); |
55 (tac, (ist, ctxt), ptp); |