263 |
263 |
264 Test_Tool.show_pt pt; (*ATTENTION: omits the last step, if pt is incomplete, ([2], Res) EXISTS !*) |
264 Test_Tool.show_pt pt; (*ATTENTION: omits the last step, if pt is incomplete, ([2], Res) EXISTS !*) |
265 ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*) |
265 ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*) |
266 |
266 |
267 |
267 |
268 (**** maximum example with Step.specify_do_next ########################################## ****) |
268 (*** maximum example with Step.specify_do_next ============================================= ***); |
269 "----------- maximum example with Step.specify_do_next -----------------------------------------"; |
269 "----------- maximum example with Step.specify_do_next -----------------------------------------"; |
270 "----------- maximum example with Step.specify_do_next -----------------------------------------"; |
270 "----------- maximum example with Step.specify_do_next -----------------------------------------"; |
271 val c = []:cid; |
271 val c = []:cid; |
272 val fmz = [ |
272 val fmz = [ |
273 "fixedValues [r=Arbfix]", "maximum A", |
273 "fixedValues [r=Arbfix]", "maximum A", |
320 |
320 |
321 (*** stepwise Specification: MethodC model ================================================ ***) |
321 (*** stepwise Specification: MethodC model ================================================ ***) |
322 val ("ok", ([(Add_Given "boundVariable a", _, _)], _, ptp)) |
322 val ("ok", ([(Add_Given "boundVariable a", _, _)], _, ptp)) |
323 = Step.specify_do_next ptp; |
323 = Step.specify_do_next ptp; |
324 Step.specify_do_next ptp; |
324 Step.specify_do_next ptp; |
325 val ("ok", ([(Add_Given "interval ({x. 0 \<le> x \<and> x \<le> 2 * r})", _, _)], _, ptp)) |
325 val ("ok", ([(Add_Given "interval {x. 0 \<le> x \<and> x \<le> 2 * r}", _, _)], _, ptp)) |
326 = Step.specify_do_next ptp; |
326 = Step.specify_do_next ptp; |
327 val ("ok", ([(Add_Given "errorBound (eps = 0)", _, _)], _, ptp)) |
327 val ("ok", ([(Add_Given "errorBound (eps = 0)", _, _)], _, ptp)) |
328 = Step.specify_do_next ptp; |
328 = Step.specify_do_next ptp; |
329 |
329 |
330 val PblObj {meth, ...} = get_obj I (fst ptp) []; |
330 val PblObj {meth, ...} = get_obj I (fst ptp) []; |