1.1 --- a/src/Tools/isac/Knowledge/Equation.thy Wed Dec 14 14:20:25 2016 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Sun Dec 18 16:27:41 2016 +0100
1.3 @@ -48,14 +48,14 @@
1.4 setup {* KEStore_Elems.add_rlss [("univariate_equation_prls",
1.5 (Context.theory_name @{theory}, prep_rls @{theory} univariate_equation_prls))] *}
1.6 setup {* KEStore_Elems.add_pbts
1.7 - [(prep_pbt thy "pbl_equ" [] e_pblID
1.8 + [(Specify.prep_pbt thy "pbl_equ" [] e_pblID
1.9 (["equation"],
1.10 [("#Given" ,["equality e_e","solveFor v_v"]),
1.11 ("#Where" ,["matches (?a = ?b) e_e"]),
1.12 ("#Find" ,["solutions v_v'i'"])],
1.13 append_rls "equation_prls" e_rls [Calc ("Tools.matches",eval_matches "")],
1.14 SOME "solve (e_e::bool, v_v)", [])),
1.15 - (prep_pbt thy "pbl_equ_univ" [] e_pblID
1.16 + (Specify.prep_pbt thy "pbl_equ_univ" [] e_pblID
1.17 (["univariate","equation"],
1.18 [("#Given" ,["equality e_e","solveFor v_v"]),
1.19 ("#Where" ,["matches (?a = ?b) e_e"]),
1.20 @@ -86,7 +86,7 @@
1.21
1.22
1.23 setup {* KEStore_Elems.add_mets
1.24 - [prep_met thy "met_equ" [] e_metID
1.25 + [Specify.prep_met thy "met_equ" [] e_metID
1.26 (["Equation"], [],
1.27 {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls,
1.28 errpats = [], nrls = e_rls},