208 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; |
208 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; |
209 ------------------------------ FIXXXXME.meNEW !!! ---*) |
209 ------------------------------ FIXXXXME.meNEW !!! ---*) |
210 |
210 |
211 (*val nxt = Specify_Theory "DiffApp.thy" : tac*) |
211 (*val nxt = Specify_Theory "DiffApp.thy" : tac*) |
212 |
212 |
213 val itms = get_obj g_pbl pt (fst p);writeln(itms2str thy itms); |
213 val itms = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt itms); |
214 |
214 |
215 val nxt = tac2tac_ pt p nxt; |
215 val nxt = tac2tac_ pt p nxt; |
216 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; |
216 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; |
217 (*val nxt = Specify_Problem ["maximum_of","function"]*) |
217 (*val nxt = Specify_Problem ["maximum_of","function"]*) |
218 |
218 |