21 "Constants [r = (7::real)]", "Maximum A", "AdditionalValues [u, v]", |
21 "Constants [r = (7::real)]", "Maximum A", "AdditionalValues [u, v]", |
22 "Extremum (A = 2 * u * v - u \<up> 2)", |
22 "Extremum (A = 2 * u * v - u \<up> 2)", |
23 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", |
23 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", |
24 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", |
24 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", |
25 "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]", |
25 "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]", |
26 (*MethodC model:*) |
26 (*MethodC model:*) |
27 "FunctionVariable a", "FunctionVariable b", "FunctionVariable \<alpha>", |
27 "FunctionVariable a", "FunctionVariable b", "FunctionVariable \<alpha>", |
28 "Domain {0 <..< r}", |
28 "Domain {0 <..< r}", |
29 "Domain {0 <..< r}", |
29 "Domain {0 <..< r}", |
30 "Domain {0 <..< \<pi> / 2}", |
30 "Domain {0 <..< \<pi> / 2}", |
31 "ErrorBound (\<epsilon> = (0::real))" |
31 "ErrorBound (\<epsilon> = (0::real))" |
38 |
38 |
39 (*/------- start example as usual in tests ---------------------------------------------------* ) |
39 (*/------- start example as usual in tests ---------------------------------------------------* ) |
40 val (p,_,f, nxt,_,pt) = CalcTreeTEST [(fmz, refs)]; |
40 val (p,_,f, nxt,_,pt) = CalcTreeTEST [(fmz, refs)]; |
41 val ptp = (pt, p); |
41 val ptp = (pt, p); |
42 ( *-------- outcomment EITHER above OR below --------------------------------------------------*) |
42 ( *-------- outcomment EITHER above OR below --------------------------------------------------*) |
43 case get_example "Diff_App/No.123 a" of |
43 case Store.get (KEStore_Elems.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"] of |
44 (_, ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" :: _, |
44 (_, ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" :: _, |
45 ("Diff_App", ["univariate_calculus", "Optimisation"] ,["Optimisation", "by_univariate_calculus"]))) |
45 ("Diff_App", ["univariate_calculus", "Optimisation"] ,["Optimisation", "by_univariate_calculus"]))) |
46 => () |
46 => () |
47 | _ => error "intermed. example_store CHANGED"; |
47 | _ => error "intermed. example_store CHANGED"; |
48 val p = ([], Pbl); |
48 val p = ([], Pbl); |
49 val pt = update_state (*here we have Ctree.EmptyPtree and thus call init_ctree*) |
49 val pt = update_state (*here we have Ctree.EmptyPtree and thus call init_ctree*) |
50 ("Diff_App/No.123 a", |
50 ("Diff_App-No.123a", |
51 (* Problem.parse_model_input results in markup, which is accepted by \<open>fun update_state\<close>, too: |
51 (* Problem.parse_model_input results in markup, which is accepted by \<open>fun update_state\<close>, too: |
52 Constants [r = 7] *) |
52 Constants [r = 7] *) |
53 ( [("#Given", ["Constants [r = 7]"]), |
53 ( [("#Given", ["Constants [r = 7]"]), |
54 ("#Where", ["0 < r"]), |
54 ("#Where", ["0 < r"]), |
55 ("#Find", ["Maximum A", "AdditionalValues [u, v]"]), |
55 ("#Find", ["Maximum A", "AdditionalValues [u, v]"]), |