1.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy	Mon Jan 27 21:58:57 2014 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy	Mon Jan 27 22:26:51 2014 +0100
     1.3 @@ -76,66 +76,8 @@
     1.4      }:rls);
     1.5  *}
     1.6  setup {* KEStore_Elems.add_rlss [("eval_rls", (Context.theory_name @{theory}, eval_rls))] *}
     1.7 -ML{*
     1.8  
     1.9  (** problem types **)
    1.10 -
    1.11 -store_pbt
    1.12 - (prep_pbt thy "pbl_fun_max" [] e_pblID
    1.13 - (["maximum_of","function"],
    1.14 -  [("#Given" ,["fixedValues f_ix"]),
    1.15 -   ("#Find"  ,["maximum m_m","valuesFor v_s"]),
    1.16 -   ("#Relate",["relations r_s"])
    1.17 -  ],
    1.18 -  e_rls, NONE, []));
    1.19 -
    1.20 -store_pbt
    1.21 - (prep_pbt thy "pbl_fun_make" [] e_pblID
    1.22 - (["make","function"]:pblID,
    1.23 -  [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
    1.24 -   ("#Find"  ,["functionEq f_1"])
    1.25 -  ],
    1.26 -  e_rls, NONE, []));
    1.27 -store_pbt
    1.28 - (prep_pbt thy "pbl_fun_max_expl" [] e_pblID
    1.29 - (["by_explicit","make","function"]:pblID,
    1.30 -  [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
    1.31 -   ("#Find"  ,["functionEq f_1"])
    1.32 -  ],
    1.33 -  e_rls, NONE, [["DiffApp","make_fun_by_explicit"]]));
    1.34 -store_pbt
    1.35 - (prep_pbt thy "pbl_fun_max_newvar" [] e_pblID
    1.36 - (["by_new_variable","make","function"]:pblID,
    1.37 -  [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
    1.38 -   (*WN.12.5.03: precond for distinction still missing*)
    1.39 -   ("#Find"  ,["functionEq f_1"])
    1.40 -  ],
    1.41 -  e_rls, NONE, [["DiffApp","make_fun_by_new_variable"]]));
    1.42 -
    1.43 -store_pbt
    1.44 - (prep_pbt thy "pbl_fun_max_interv" [] e_pblID
    1.45 - (["on_interval","maximum_of","function"]:pblID,
    1.46 -  [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"]),
    1.47 -   (*WN.12.5.03: precond for distinction still missing*)
    1.48 -   ("#Find"  ,["maxArgument v_0"])
    1.49 -  ],
    1.50 -  e_rls, NONE, []));
    1.51 -
    1.52 -store_pbt
    1.53 - (prep_pbt thy "pbl_tool" [] e_pblID
    1.54 - (["tool"]:pblID,
    1.55 -  [],
    1.56 -  e_rls, NONE, []));
    1.57 -
    1.58 -store_pbt
    1.59 - (prep_pbt thy "pbl_tool_findvals" [] e_pblID
    1.60 - (["find_values","tool"]:pblID,
    1.61 -  [("#Given" ,["maxArgument m_ax","functionEq f_f","boundVariable v_v"]),
    1.62 -   ("#Find"  ,["valuesFor v_ls"]),
    1.63 -   ("#Relate",["additionalRels r_s"])
    1.64 -  ],
    1.65 -  e_rls, NONE, []));
    1.66 -*}
    1.67  setup {* KEStore_Elems.add_pbts
    1.68    [(prep_pbt thy "pbl_fun_max" [] e_pblID
    1.69        (["maximum_of","function"],