1.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy	Mon Jan 20 16:15:34 2014 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy	Tue Jan 21 00:27:44 2014 +0100
     1.3 @@ -135,8 +135,44 @@
     1.4     ("#Relate",["additionalRels r_s"])
     1.5    ],
     1.6    e_rls, NONE, []));
     1.7 -
     1.8  *}
     1.9 +setup {* KEStore_Elems.store_pbts
    1.10 +  [(prep_pbt thy "pbl_fun_max" [] e_pblID
    1.11 +      (["maximum_of","function"],
    1.12 +        [("#Given" ,["fixedValues f_ix"]),
    1.13 +          ("#Find"  ,["maximum m_m","valuesFor v_s"]),
    1.14 +          ("#Relate",["relations r_s"])],
    1.15 +        e_rls, NONE, [])),
    1.16 +    (prep_pbt thy "pbl_fun_make" [] e_pblID
    1.17 +      (["make","function"]:pblID,
    1.18 +        [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
    1.19 +          ("#Find"  ,["functionEq f_1"])],
    1.20 +        e_rls, NONE, [])),
    1.21 +    (prep_pbt thy "pbl_fun_max_expl" [] e_pblID
    1.22 +      (["by_explicit","make","function"]:pblID,
    1.23 +        [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
    1.24 +          ("#Find"  ,["functionEq f_1"])],
    1.25 +      e_rls, NONE, [["DiffApp","make_fun_by_explicit"]])),
    1.26 +    (prep_pbt thy "pbl_fun_max_newvar" [] e_pblID
    1.27 +      (["by_new_variable","make","function"]:pblID,
    1.28 +        [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
    1.29 +          (*WN.12.5.03: precond for distinction still missing*)
    1.30 +          ("#Find"  ,["functionEq f_1"])],
    1.31 +      e_rls, NONE, [["DiffApp","make_fun_by_new_variable"]])),
    1.32 +    (prep_pbt thy "pbl_fun_max_interv" [] e_pblID
    1.33 +      (["on_interval","maximum_of","function"]:pblID,
    1.34 +        [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"]),
    1.35 +          (*WN.12.5.03: precond for distinction still missing*)
    1.36 +          ("#Find"  ,["maxArgument v_0"])],
    1.37 +      e_rls, NONE, [])),
    1.38 +    (prep_pbt thy "pbl_tool" [] e_pblID
    1.39 +      (["tool"]:pblID, [], e_rls, NONE, [])),
    1.40 +    (prep_pbt thy "pbl_tool_findvals" [] e_pblID
    1.41 +      (["find_values","tool"]:pblID,
    1.42 +        [("#Given" ,["maxArgument m_ax","functionEq f_f","boundVariable v_v"]),
    1.43 +          ("#Find"  ,["valuesFor v_ls"]),
    1.44 +          ("#Relate",["additionalRels r_s"])],
    1.45 +      e_rls, NONE, []))] *}
    1.46  ML{*
    1.47  
    1.48  (** methods, scripts not yet implemented **)