530 (*if*) p_ = Pos.Pbl (*else*); |
530 (*if*) p_ = Pos.Pbl (*else*); |
531 val return = for_problem ctxt oris (o_refs, refs) (pbl, met); |
531 val return = for_problem ctxt oris (o_refs, refs) (pbl, met); |
532 "~~~~~ fun for_method , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) = |
532 "~~~~~ fun for_method , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) = |
533 (oris, (o_refs, refs), (pbl, met)); |
533 (oris, (o_refs, refs), (pbl, met)); |
534 val cmI = if mI = MethodC.id_empty then mI' else mI; |
534 val cmI = if mI = MethodC.id_empty then mI' else mI; |
535 val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI; (*..MethodC ?*) |
535 val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI; |
536 val (preok, _) = Pre_Conds.check ctxt where_rls where_ pbl 0; |
536 val (preok, _) = Pre_Conds.check_OLD ctxt where_rls where_ (mpc, I_Model.OLD_to_TEST met); |
537 "~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) = (return); |
537 "~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) = (return); |
538 (*/------------------- check within find_next_step -----------------------------------------\*) |
538 (*/------------------- check within find_next_step -----------------------------------------\*) |
539 (*+*)Model_Pattern.to_string @{context} (MethodC.from_store ctxt mI' |> #model) = "[\"" ^ |
539 (*+*)Model_Pattern.to_string @{context} (MethodC.from_store ctxt mI' |> #model) = "[\"" ^ |
540 "(#Given, (Traegerlaenge, l))\", \"" ^ |
540 "(#Given, (Traegerlaenge, l))\", \"" ^ |
541 "(#Given, (Streckenlast, q))\", \"" ^ |
541 "(#Given, (Streckenlast, q))\", \"" ^ |