src/Tools/isac/Knowledge/Equation.thy
changeset 59269 1da53d1540fe
parent 59186 d9c3e373f8f5
child 59279 255c853ea2f0
     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},