1.1 --- a/src/Tools/isac/Interpret/appl.sml Fri May 20 14:08:14 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/appl.sml Fri May 20 14:49:07 2011 +0200
1.3 @@ -347,26 +347,21 @@
1.4 if is_e_ctxt ctxt
1.5 then assoc_thy dI |> ProofContext.init_global |> insert_assumptions pres
1.6 else ctxt
1.7 - (*TODO.WN110416 here do evalprecond according to fun check_preconds'
1.8 - and then decide on Notappl/Appl accordingly once more.
1.9 - Implement after all tests are running, since this changes
1.10 - overall system behavior*)
1.11 - in Appl (Apply_Method' (mI, NONE, e_istate (*filled in solve*), ctxt)) end
1.12 + (*TODO.WN110416 here do evalprecond according to fun check_preconds'
1.13 + and then decide on Notappl/Appl accordingly once more.
1.14 + Implement after all tests are running, since this changes
1.15 + overall system behavior*)
1.16 + in Appl (Apply_Method' (mI, NONE, e_istate (*filled in solve*), ctxt)) end
1.17
1.18 | applicable_in (p,p_) pt (Check_Postcond pI) =
1.19 - if member op = [Pbl,Met] p_
1.20 - then Notappl ((tac2str (Check_Postcond pI)) ^
1.21 - " not for pos "^(pos'2str (p,p_)))
1.22 - else Appl (Check_Postcond'
1.23 - (pI,(e_term,[(*asm in solve*)])))
1.24 - (* in solve -"- ^^^^^^ gets returnvalue of scr*)
1.25 + if member op = [Pbl,Met] p_
1.26 + then Notappl ((tac2str (Check_Postcond pI)) ^ " not for pos "^(pos'2str (p,p_)))
1.27 + else Appl (Check_Postcond' (pI, (e_term, [(*in solve assigned the returnvalue of scr*)])))
1.28
1.29 (*these are always applicable*)
1.30 | applicable_in (p,p_) _ (Take str) = Appl (Take' (str2term str))
1.31 | applicable_in (p,p_) _ (Free_Solve) = Appl (Free_Solve')
1.32
1.33 -(* val m as Rewrite_Inst (subs, thm') = m;
1.34 - *)
1.35 | applicable_in (p,p_) pt (m as Rewrite_Inst (subs, thm')) =
1.36 if member op = [Pbl,Met] p_
1.37 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
2.1 --- a/src/Tools/isac/Interpret/ctree.sml Fri May 20 14:08:14 2011 +0200
2.2 +++ b/src/Tools/isac/Interpret/ctree.sml Fri May 20 14:49:07 2011 +0200
2.3 @@ -558,7 +558,7 @@
2.4 | Check_Postcond' of
2.5 pblID *
2.6 (term * (*returnvalue of script in solve*)
2.7 - cterm' list)(*collect by get_assumptions_ in applicable_in, except if
2.8 + term list) (*collect by get_assumptions_ in applicable_in, except if
2.9 butlast tac is Check_elementwise: take only these asms*)
2.10 | Free_Solve'
2.11
2.12 @@ -647,8 +647,8 @@
2.13
2.14 | Apply_Method' (metID,_,_,_) => "Apply_Method' "^(strs2str metID)
2.15 | Check_Postcond' (pblID,(scval,asm)) =>
2.16 - "Check_Postcond' "^(spair2str(strs2str pblID,
2.17 - spair2str (term2str scval, strs2str asm)))
2.18 + "Check_Postcond' " ^
2.19 + (spair2str (strs2str pblID, spair2str (term2str scval, terms2str asm)))
2.20
2.21 | Free_Solve' => "Free_Solve'"
2.22
3.1 --- a/src/Tools/isac/Interpret/generate.sml Fri May 20 14:08:14 2011 +0200
3.2 +++ b/src/Tools/isac/Interpret/generate.sml Fri May 20 14:49:07 2011 +0200
3.3 @@ -441,8 +441,8 @@
3.4 val pos' = ((lev_on o lev_dn) p, Frm)
3.5 in (*implicit Take*) generate1 thy tac_ (is, ctxt) pos' pt end
3.6
3.7 - | generate1 thy (Check_Postcond' (pI,(scval,asm))) l (p,p_) pt =
3.8 - let val (pt,c) = append_result pt p l (scval, map str2term asm) Complete
3.9 + | generate1 thy (Check_Postcond' (pI, (scval, asm))) l (p,p_) pt =
3.10 + let val (pt,c) = append_result pt p l (scval, asm) Complete
3.11 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p),
3.12 Nundef, term2str scval)), pt) end
3.13
4.1 --- a/src/Tools/isac/Interpret/script.sml Fri May 20 14:08:14 2011 +0200
4.2 +++ b/src/Tools/isac/Interpret/script.sml Fri May 20 14:49:07 2011 +0200
4.3 @@ -652,28 +652,22 @@
4.4 | tac_2tac (Specify_Problem' (dI,_)) = Specify_Problem dI
4.5 | tac_2tac (Specify_Method' (dI,_,_)) = Specify_Method dI
4.6
4.7 - | tac_2tac (Rewrite' (thy,rod,erls,put,(thmID,thm),f,(f',asm))) =
4.8 - Rewrite (thmID,thm)
4.9 + | tac_2tac (Rewrite' (thy,rod,erls,put,(thmID,thm),f,(f',asm))) = Rewrite (thmID,thm)
4.10
4.11 | tac_2tac (Rewrite_Inst' (thy,rod,erls,put,sub,(thmID,thm),f,(f',asm)))=
4.12 - Rewrite_Inst (subst2subs sub,(thmID,thm))
4.13 + Rewrite_Inst (subst2subs sub,(thmID,thm))
4.14
4.15 - | tac_2tac (Rewrite_Set' (thy,put,rls,f,(f',asm))) =
4.16 - Rewrite_Set (id_rls rls)
4.17 -
4.18 - | tac_2tac (Detail_Set' (thy,put,rls,f,(f',asm))) =
4.19 - Detail_Set (id_rls rls)
4.20 + | tac_2tac (Rewrite_Set' (thy,put,rls,f,(f',asm))) = Rewrite_Set (id_rls rls)
4.21 + | tac_2tac (Detail_Set' (thy,put,rls,f,(f',asm))) = Detail_Set (id_rls rls)
4.22
4.23 | tac_2tac (Rewrite_Set_Inst' (thy,put,sub,rls,f,(f',asm))) =
4.24 - Rewrite_Set_Inst (subst2subs sub,id_rls rls)
4.25 -
4.26 + Rewrite_Set_Inst (subst2subs sub,id_rls rls)
4.27 | tac_2tac (Detail_Set_Inst' (thy,put,sub,rls,f,(f',asm))) =
4.28 - Detail_Set_Inst (subst2subs sub,id_rls rls)
4.29 + Detail_Set_Inst (subst2subs sub,id_rls rls)
4.30
4.31 | tac_2tac (Calculate' (thy,op_,t,(t',thm'))) = Calculate (op_)
4.32
4.33 - | tac_2tac (Check_elementwise' (consts,pred,consts')) =
4.34 - Check_elementwise pred
4.35 + | tac_2tac (Check_elementwise' (consts,pred,consts')) = Check_elementwise pred
4.36
4.37 | tac_2tac (Or_to_List' _) = Or_to_List
4.38 | tac_2tac (Take' term) = Take (term2str term)
4.39 @@ -681,14 +675,11 @@
4.40
4.41 | tac_2tac (Tac_ (_,f,id,f')) = Tac id
4.42
4.43 - | tac_2tac (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) =
4.44 - Subproblem (domID, pblID)
4.45 - | tac_2tac (Check_Postcond' (pblID, _)) =
4.46 - Check_Postcond pblID
4.47 + | tac_2tac (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) = Subproblem (domID, pblID)
4.48 + | tac_2tac (Check_Postcond' (pblID, _)) = Check_Postcond pblID
4.49 | tac_2tac Empty_Tac_ = Empty_Tac
4.50 -
4.51 | tac_2tac m =
4.52 - error ("tac_2tac: not impl. for "^(tac_2str m));
4.53 + error ("tac_2tac: not impl. for "^(tac_2str m));
4.54
4.55
4.56
5.1 --- a/src/Tools/isac/Interpret/solve.sml Fri May 20 14:08:14 2011 +0200
5.2 +++ b/src/Tools/isac/Interpret/solve.sml Fri May 20 14:49:07 2011 +0200
5.3 @@ -181,8 +181,8 @@
5.4 in ("ok", ([(Empty_Tac, Empty_Tac_, (po, (Uistate, e_ctxt)))], [], (pt,p')))
5.5 end
5.6
5.7 - | solve ("Check_Postcond",Check_Postcond' (pI,_)) (pt,(pos as (p,p_))) =
5.8 - let (*val _=tracing"###solve Check_Postcond";*)
5.9 + | solve ("Check_Postcond", Check_Postcond' (pI,_)) (pt,(pos as (p,p_))) =
5.10 + let
5.11 val pp = par_pblobj pt p
5.12 val asm =
5.13 (case get_obj g_tac pt p of
5.14 @@ -201,7 +201,7 @@
5.15 then
5.16 let
5.17 val is = ScrState (E,l,a,scval,scsaf,b)
5.18 - val tac_ = Check_Postcond'(pI,(scval, map term2str asm))
5.19 + val tac_ = Check_Postcond' (pI, (scval, asm))
5.20 val (pos,ps,f,pt) = generate1 thy tac_ (is, ctxt) (pp,Res) pt;
5.21 in ("ok", ([(Check_Postcond pI, tac_, ((pp,Res),(is, ctxt)))], ps,(pt,pos))) end
5.22 else
5.23 @@ -214,9 +214,9 @@
5.24 val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm);
5.25 val ctxt'' = transfer_from_subproblem ctxt ctxt'
5.26 val ((p,p_),ps,f,pt) =
5.27 - generate1 thy (Check_Postcond' (pI, (scval, map term2str asm)))
5.28 + generate1 thy (Check_Postcond' (pI, (scval, asm)))
5.29 (ScrState (E,l,a,scval,scsaf,b), ctxt'') (pp,Res) pt;
5.30 - in ("ok", ([(Check_Postcond pI, Check_Postcond'(pI,(scval, map term2str asm)),
5.31 + in ("ok", ([(Check_Postcond pI, Check_Postcond'(pI,(scval, asm)),
5.32 ((pp,Res), (ScrState (E,l,a,scval,scsaf,b), ctxt'')))],ps,(pt,(p,p_))))
5.33 end
5.34 end
5.35 @@ -320,7 +320,7 @@
5.36 then
5.37 let
5.38 val is = ScrState (E,l,a,scval,scsaf,b)
5.39 - val tac_ = Check_Postcond'(pI,(scval, map term2str asm))
5.40 + val tac_ = Check_Postcond'(pI,(scval, asm))
5.41 val ((p,p_),ps,f,pt) =
5.42 generate1 thy tac_ (is, ctxt) (pp,Res) pt;
5.43 in ([(Check_Postcond pI, tac_, ((pp,Res), (is, ctxt)))],ps,(pt, (p,p_))) end
5.44 @@ -333,7 +333,7 @@
5.45 val {scr,...} = get_met metID;
5.46 val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm)
5.47 val ctxt'' = transfer_from_subproblem ctxt ctxt'
5.48 - val tac_ = Check_Postcond' (pI, (scval, map term2str asm))
5.49 + val tac_ = Check_Postcond' (pI, (scval, asm))
5.50 val is = ScrState (E,l,a,scval,scsaf,b)
5.51 val ((p,p_),ps,f,pt) = generate1 thy tac_ (is, ctxt'') (pp, Res) pt;
5.52 in ([(Check_Postcond pI, tac_, ((pp, Res), (is, ctxt'')))], ps, (pt, (p,p_))) end
6.1 --- a/test/Tools/isac/Minisubpbl/600-postcond.sml Fri May 20 14:08:14 2011 +0200
6.2 +++ b/test/Tools/isac/Minisubpbl/600-postcond.sml Fri May 20 14:49:07 2011 +0200
6.3 @@ -9,29 +9,29 @@
6.4 ["Test","squ-equ-test-subpbl1"]);
6.5 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.6 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.7 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.8 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.9 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.10 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.11 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.12 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.13 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.14 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.15 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Subproblem"*)
6.16 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.17 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.18 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.19 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.20 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.21 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.22 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.23 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.24 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.25 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.26 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.27 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.28 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.29 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.30 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.31 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.32 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.33 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.34 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.35 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.36 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.37 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.38 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)
6.39 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.40 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.41 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.42 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.43 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.44 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.45 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.46 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.47 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.48 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.49 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.50 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.51 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.52 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.53 if nxt = ("End_Proof'", End_Proof') andalso p = ([], Res)
6.54 andalso get_obj g_res pt (fst p) = str2term "[x=1]" then ()
6.55 else error "calculation not finished correctly";
7.1 --- a/test/Tools/isac/Test_Isac.thy Fri May 20 14:08:14 2011 +0200
7.2 +++ b/test/Tools/isac/Test_Isac.thy Fri May 20 14:49:07 2011 +0200
7.3 @@ -165,136 +165,13 @@
7.4 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
7.5
7.6 ML {*
7.7 -*}
7.8 -ML {*
7.9 -"----------- Minisubplb/500-met-sub-to-root.sml ------------------";
7.10 -
7.11 -"----------- Minisubplb/450-nxt-Check_Postcond -------------------";
7.12 -val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
7.13 -val (dI',pI',mI') =
7.14 - ("Test", ["sqroot-test","univariate","equation","test"],
7.15 - ["Test","squ-equ-test-subpbl1"]);
7.16 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.17 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.18 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.19 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.20 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.21 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.22 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.23 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
7.24 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.25 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.26 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["linear", "univariate", "equation", "test"]*)
7.27 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.28 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.29 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.30 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.31 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.32 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.33 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.34 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
7.35 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst isolate_bdv*);
7.36 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*);
7.37 -val (pt''''', p''''') = (pt, p);
7.38 -
7.39 -"~~~~~ fun me, args:"; val (_,tac) = nxt;
7.40 -val (pt, p) = case locatetac tac (pt,p) of
7.41 - ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
7.42 -val (pt'''', p'''') = (pt, p);
7.43 -"~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
7.44 -val pIopt = get_pblID (pt,ip); (*= SOME ["sqroot-test", "univariate", ...]*)
7.45 -tacis; (*= []*)
7.46 -val SOME pI = pIopt;
7.47 -member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
7.48 -"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
7.49 -e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
7.50 -val thy' = get_obj g_domID pt (par_pblobj pt p);
7.51 -val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
7.52 -val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is;
7.53 -;tac_; (* = Check_Postcond' *)
7.54 -"~~~~~ fun nxt_solv, args:"; val ((Check_Postcond' (pI,_)), _, (pt, pos as (p,p_))) =
7.55 - (tac_, is, ptp);
7.56 - val pp = par_pblobj pt p
7.57 - val asm =
7.58 - (case get_obj g_tac pt p of
7.59 - Check_elementwise _ => (*collects and instantiates asms*)
7.60 - (snd o (get_obj g_result pt)) p
7.61 - | _ => get_assumptions_ pt (p,p_))
7.62 - handle _ => [] (*FIXME.WN030527 asms in subpbls not completely clear*)
7.63 - val metID = get_obj g_metID pt pp;
7.64 - val {srls=srls,scr=sc,...} = get_met metID;
7.65 - val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_);
7.66 - val thy' = get_obj g_domID pt pp;
7.67 - val thy = assoc_thy thy';
7.68 - val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc loc;
7.69 -*}
7.70 -ML {*
7.71 -;pp = []; (*false*)
7.72 - val ppp = par_pblobj pt (lev_up p);
7.73 - val thy' = get_obj g_domID pt ppp;
7.74 - val thy = assoc_thy thy';
7.75 - val metID = get_obj g_metID pt ppp;
7.76 - val {scr,...} = get_met metID;
7.77 - val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm)
7.78 - val ctxt'' = transfer_from_subproblem ctxt ctxt'
7.79 - val tac_ = Check_Postcond' (pI, (scval, map term2str asm))
7.80 - val is = ScrState (E,l,a,scval,scsaf,b)
7.81 -*}
7.82 -ML {*
7.83 -"~~~~~ fun generate1, args:"; val (thy, (Check_Postcond' (pI,(scval,asm))), l, (p,p_), pt) = (thy, tac_, (is, ctxt''), (pp, Res), pt);
7.84 -*}
7.85 -ML {*
7.86 -append_result pt p l
7.87 -*}
7.88 -ML {*
7.89 -asm
7.90 -*}
7.91 -ML {*
7.92 -*}
7.93 -ML {*
7.94 -scval
7.95 -*}
7.96 -ML {*
7.97 -(*
7.98 -val (pt,c) = append_result pt p l (scval, map str2term asm) Complete
7.99 -*)
7.100 -*}
7.101 -ML {*
7.102 -*}
7.103 -ML {*
7.104 -fun str2term str = (term_of o the o (parse (Thy_Info.get_theory "Isac"))) str;
7.105 -val (thy, str) = (@{theory}, "matches (?a = ?b) (x+1=2)")
7.106 -*}
7.107 -ML {*
7.108 -fun str2term str = parse_patt (Thy_Info.get_theory "Isac") str
7.109 -*}
7.110 -ML {*
7.111 +insert_assumptions
7.112 *}
7.113 ML {*
7.114 *}
7.115 ML {*
7.116 *}
7.117
7.118 -
7.119 -
7.120 -
7.121 -
7.122 -
7.123 -
7.124 -ML {*
7.125 -generate1 thy tac_ (is, ctxt'') (pp, Res) pt; (*WAS
7.126 - exception Option raised (line 81 of "General/basics.ML")*)
7.127 -*}
7.128 -ML {*
7.129 -(*
7.130 -;nxt_solv tac_ is ptp; (*WAS exception Option raised (line 81 of "General/basics.ML")*)
7.131 -*)
7.132 -*}
7.133 -ML {*
7.134 -;step p'''' ((pt'''', e_pos'),[]); (* WAS = ("helpless", *)
7.135 -val (p,_,f,nxt,_,pt) = me nxt p''''' [] pt'''''; (*nxt = Check_Postcond ["linear","uval (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)nivariate", ...]) *);
7.136 -show_pt pt
7.137 -*}
7.138 end
7.139
7.140 (*=== inhibit exn ?=============================================================