| changeset 60778 | 41abd196342a |
| parent 60766 | 2e0603ca18a4 |
| child 60780 | 91b105cf194a |
| 60777:df8636ffd6f8 | 60778:41abd196342a |
|---|---|
301 = Step.specify_do_next ptp; |
301 = Step.specify_do_next ptp; |
302 |
302 |
303 (*** Problem model is complete ============================================================ ***) |
303 (*** Problem model is complete ============================================================ ***) |
304 val PblObj {probl, ...} = get_obj I (fst ptp) []; |
304 val PblObj {probl, ...} = get_obj I (fst ptp) []; |
305 |
305 |
306 if I_Model.to_string @{context} probl = "[\n" ^ |
306 val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS fixedValues [r = Arbfix] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS valuesFor [a, b] , pen2str, Position.T)), \n(4, [1, 2], true ,#Relate, (Cor_POS relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] , pen2str, Position.T))]" |
307 "(1 ,[1, 2, 3] ,true ,#Given ,Cor fixedValues [r = Arbfix] , pen2str), \n" ^ |
307 = probl |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt |
308 "(2 ,[1, 2, 3] ,true ,#Find ,Cor maximum A , pen2str), \n" ^ |
|
309 "(3 ,[1, 2, 3] ,true ,#Find ,Cor valuesFor [a, b] , pen2str), \n" ^ |
|
310 "(4 ,[1, 2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] , pen2str)]" |
|
311 then () else error "I_Model.to_string probl CHANGED"; |
|
312 |
308 |
313 (*** Specification of References ========================================================== ***) |
309 (*** Specification of References ========================================================== ***) |
314 val ("ok", ([(Specify_Theory "Diff_App", _, _)], _, ptp)) |
310 val ("ok", ([(Specify_Theory "Diff_App", _, _)], _, ptp)) |
315 = Step.specify_do_next ptp; |
311 = Step.specify_do_next ptp; |
316 val ("ok", ([(Specify_Problem ["maximum_of", "function"], _, _)], _, ptp)) |
312 val ("ok", ([(Specify_Problem ["maximum_of", "function"], _, _)], _, ptp)) |
327 val ("ok", ([(Add_Given "errorBound (eps = 0)", _, _)], _, ptp)) |
323 val ("ok", ([(Add_Given "errorBound (eps = 0)", _, _)], _, ptp)) |
328 = Step.specify_do_next ptp; |
324 = Step.specify_do_next ptp; |
329 |
325 |
330 val PblObj {meth, ...} = get_obj I (fst ptp) []; |
326 val PblObj {meth, ...} = get_obj I (fst ptp) []; |
331 |
327 |
332 (*+*)val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor fixedValues [r = Arbfix] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor maximum A , pen2str), \n(4 ,[1, 2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] , pen2str), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor valuesFor [a, b] , pen2str), \n(6 ,[1] ,true ,#Given ,Cor boundVariable a , pen2str), \n(9 ,[1, 2] ,true ,#Given ,Cor interval {x. 0 \<le> x \<and> x \<le> 2 * r} , pen2str), \n(11 ,[1, 2, 3] ,true ,#Given ,Cor errorBound (eps = 0) , pen2str)]" |
328 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS fixedValues [r = Arbfix] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS maximum A , pen2str, Position.T)), \n(4, [1, 2], true ,#Relate, (Cor_POS relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS valuesFor [a, b] , pen2str, Position.T)), \n(6, [1], true ,#Given, (Cor_POS boundVariable a , pen2str, Position.T)), \n(9, [1, 2], true ,#Given, (Cor_POS interval {x. 0 \<le> x \<and> x \<le> 2 * r} , pen2str, Position.T)), \n(11, [1, 2, 3], true ,#Given, (Cor_POS errorBound (eps = 0) , pen2str, Position.T))]" |
333 = meth |> I_Model.to_string @{context} |
329 = meth |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt |
334 |
330 |
335 (*** Specification of Problem and MethodC model is complete, Solution starts ============== ***) |
331 (*** Specification of Problem and MethodC model is complete, Solution starts ============== ***) |
336 |
332 |
337 (* Step.specify_do_next ptp; |
333 (* Step.specify_do_next ptp; |
338 ERROR |
334 ERROR |