43 (Cor_POS ((@{term "Constants"}, [@{term "[r = (7::real)]"(*should be "r = (7::real)"*)}])), Position.none )) :: |
43 (Cor_POS ((@{term "Constants"}, [@{term "[r = (7::real)]"(*should be "r = (7::real)"*)}])), Position.none )) :: |
44 nth 2 probl :: nth 3 probl :: nth 4 probl :: |
44 nth 2 probl :: nth 3 probl :: nth 4 probl :: |
45 (5, [1,2], true, "#Relate", |
45 (5, [1,2], true, "#Relate", |
46 (Cor_POS ((@{term "SideConditions"}, [@{term "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"}])), Position.none )) |
46 (Cor_POS ((@{term "SideConditions"}, [@{term "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"}])), Position.none )) |
47 :: [] : I_Model.T_POS; |
47 :: [] : I_Model.T_POS; |
48 val probl_OLD = I_Model.TEST_to_OLD probl : I_Model.T; |
48 val probl_OLD = probl |
49 |
49 |
50 val {model = model_patt, where_rls, where_ = where_OLD, ...} = (*from_store without Position.T-vv*) |
50 val {model = model_patt, where_rls, where_ = where_OLD, ...} = (*from_store without Position.T-vv*) |
51 Problem.from_store ctxt (References.explode_id "univariate_calculus/Optimisation") |
51 Problem.from_store ctxt (References.explode_id "univariate_calculus/Optimisation") |
52 ; |
52 ; |
53 if (model_patt |> Model_Pattern.to_string ctxt) = |
53 if (model_patt |> Model_Pattern.to_string ctxt) = |