src/Tools/isac/Knowledge/DiffApp.thy
changeset 55359 73dc85c025ab
parent 55339 cccd24e959ba
child 55363 d78bc1342183
equal deleted inserted replaced
55358:b1f0389ca11f 55359:73dc85c025ab
   134    ("#Find"  ,["valuesFor v_ls"]),
   134    ("#Find"  ,["valuesFor v_ls"]),
   135    ("#Relate",["additionalRels r_s"])
   135    ("#Relate",["additionalRels r_s"])
   136   ],
   136   ],
   137   e_rls, NONE, []));
   137   e_rls, NONE, []));
   138 *}
   138 *}
   139 setup {* KEStore_Elems.store_pbts
   139 setup {* KEStore_Elems.add_pbts
   140   [(prep_pbt thy "pbl_fun_max" [] e_pblID
   140   [(prep_pbt thy "pbl_fun_max" [] e_pblID
   141       (["maximum_of","function"],
   141       (["maximum_of","function"],
   142         [("#Given" ,["fixedValues f_ix"]),
   142         [("#Given" ,["fixedValues f_ix"]),
   143           ("#Find"  ,["maximum m_m","valuesFor v_s"]),
   143           ("#Find"  ,["maximum m_m","valuesFor v_s"]),
   144           ("#Relate",["relations r_s"])],
   144           ("#Relate",["relations r_s"])],