18 oben :: real |
18 oben :: real |
19 senkrecht :: real |
19 senkrecht :: real |
20 unten :: real |
20 unten :: real |
21 |
21 |
22 (** problems **) |
22 (** problems **) |
23 setup \<open>KEStore_Elems.add_pbts |
23 |
24 [(Problem.prep_input @{theory} "pbl_algein" [] Problem.id_empty (["Berechnung"], [], Rule_Set.empty, NONE, [])), |
24 problem pbl_algein : "Berechnung" = \<open>Rule_Set.empty\<close> |
25 (Problem.prep_input @{theory} "pbl_algein_numsym" [] Problem.id_empty |
25 |
26 (["numerischSymbolische", "Berechnung"], |
26 problem pbl_algein_numsym : "numerischSymbolische/Berechnung" = \<open>Rule_Set.empty\<close> |
27 [("#Given", |
27 Method: "Berechnung/erstNumerisch" "Berechnung/erstSymbolisch" |
28 ["KantenLaenge k_k", "Querschnitt q__q"(*q_ in Biegelinie.thy*), "KantenUnten u_u", |
28 Given: "KantenLaenge k_k" "Querschnitt q__q" (*q_ in Biegelinie.thy*) "KantenUnten u_u" |
29 "KantenSenkrecht s_s", "KantenOben o_o"]), |
29 "KantenSenkrecht s_s" "KantenOben o_o" |
30 ("#Find", ["GesamtLaenge l_l"])], |
30 Find: "GesamtLaenge l_l" |
31 Rule_Set.empty, NONE, [["Berechnung", "erstNumerisch"], ["Berechnung", "erstSymbolisch"]]))]\<close> |
|
32 |
31 |
33 method met_algein : "Berechnung" = |
32 method met_algein : "Berechnung" = |
34 \<open>{rew_ord'="tless_true", rls'= Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls =Rule_Set.Empty, |
33 \<open>{rew_ord'="tless_true", rls'= Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls =Rule_Set.Empty, |
35 errpats = [], nrls = Rule_Set.Empty}\<close> |
34 errpats = [], nrls = Rule_Set.Empty}\<close> |
36 |
35 |