37 date: 02.11.29 |
37 date: 02.11.29 |
38 (c) by Richard Lang, 2003 *} |
38 (c) by Richard Lang, 2003 *} |
39 |
39 |
40 ML {* |
40 ML {* |
41 val thy = @{theory}; |
41 val thy = @{theory}; |
42 val ctxt = thy2ctxt thy; |
42 val ctxt = Celem.thy2ctxt thy; |
43 |
43 |
44 val univariate_equation_prls = |
44 val univariate_equation_prls = |
45 append_rls "univariate_equation_prls" e_rls |
45 Celem.append_rls "univariate_equation_prls" Celem.e_rls |
46 [Calc ("Tools.matches",eval_matches "")]; |
46 [Celem.Calc ("Tools.matches",eval_matches "")]; |
47 *} |
47 *} |
48 setup {* KEStore_Elems.add_rlss [("univariate_equation_prls", |
48 setup {* KEStore_Elems.add_rlss [("univariate_equation_prls", |
49 (Context.theory_name @{theory}, LTool.prep_rls @{theory} univariate_equation_prls))] *} |
49 (Context.theory_name @{theory}, LTool.prep_rls @{theory} univariate_equation_prls))] *} |
50 setup {* KEStore_Elems.add_pbts |
50 setup {* KEStore_Elems.add_pbts |
51 [(Specify.prep_pbt thy "pbl_equ" [] e_pblID |
51 [(Specify.prep_pbt thy "pbl_equ" [] Celem.e_pblID |
52 (["equation"], |
52 (["equation"], |
53 [("#Given" ,["equality e_e","solveFor v_v"]), |
53 [("#Given" ,["equality e_e","solveFor v_v"]), |
54 ("#Where" ,["matches (?a = ?b) e_e"]), |
54 ("#Where" ,["matches (?a = ?b) e_e"]), |
55 ("#Find" ,["solutions v_v'i'"])], |
55 ("#Find" ,["solutions v_v'i'"])], |
56 append_rls "equation_prls" e_rls [Calc ("Tools.matches",eval_matches "")], |
56 Celem.append_rls "equation_prls" Celem.e_rls [Celem.Calc ("Tools.matches",eval_matches "")], |
57 SOME "solve (e_e::bool, v_v)", [])), |
57 SOME "solve (e_e::bool, v_v)", [])), |
58 (Specify.prep_pbt thy "pbl_equ_univ" [] e_pblID |
58 (Specify.prep_pbt thy "pbl_equ_univ" [] Celem.e_pblID |
59 (["univariate","equation"], |
59 (["univariate","equation"], |
60 [("#Given" ,["equality e_e","solveFor v_v"]), |
60 [("#Given" ,["equality e_e","solveFor v_v"]), |
61 ("#Where" ,["matches (?a = ?b) e_e"]), |
61 ("#Where" ,["matches (?a = ?b) e_e"]), |
62 ("#Find" ,["solutions v_v'i'"])], |
62 ("#Find" ,["solutions v_v'i'"])], |
63 univariate_equation_prls, SOME "solve (e_e::bool, v_v)", []))] *} |
63 univariate_equation_prls, SOME "solve (e_e::bool, v_v)", []))] *} |
84 ((Thm.term_of o the o (TermC.parse thy)) "solve", |
84 ((Thm.term_of o the o (TermC.parse thy)) "solve", |
85 (("Isac", ["univariate","equation"], ["no_met"]), argl2dtss))]*} |
85 (("Isac", ["univariate","equation"], ["no_met"]), argl2dtss))]*} |
86 |
86 |
87 |
87 |
88 setup {* KEStore_Elems.add_mets |
88 setup {* KEStore_Elems.add_mets |
89 [Specify.prep_met thy "met_equ" [] e_metID |
89 [Specify.prep_met thy "met_equ" [] Celem.e_metID |
90 (["Equation"], [], |
90 (["Equation"], [], |
91 {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls, |
91 {rew_ord'="tless_true", rls'=Celem.Erls, calc = [], srls = Celem.e_rls, prls=Celem.e_rls, crls = Atools_erls, |
92 errpats = [], nrls = e_rls}, |
92 errpats = [], nrls = Celem.e_rls}, |
93 "empty_script")] |
93 "empty_script")] |
94 *} |
94 *} |
95 |
95 |
96 end |
96 end |