24 \ --> m' <= m_)))") *) |
24 \ --> m' <= m_)))") *) |
25 ]), |
25 ]), |
26 |
26 |
27 prep_pbt DiffAppl.thy |
27 prep_pbt DiffAppl.thy |
28 (["DiffAppl","make","function"]:pblID, |
28 (["DiffAppl","make","function"]:pblID, |
29 [("#Given" ,"functionOf f_"), |
29 [("#Given" ,"functionOf f_f"), |
30 ("#Given" ,"boundVariable v_v"), |
30 ("#Given" ,"boundVariable v_v"), |
31 ("#Given" ,"equalities eqs_"), |
31 ("#Given" ,"equalities eqs"), |
32 ("#Find" ,"functionTerm f_0_") |
32 ("#Find" ,"functionTerm f_0_") |
33 ]), |
33 ]), |
34 |
34 |
35 prep_pbt DiffAppl.thy |
35 prep_pbt DiffAppl.thy |
36 (["DiffAppl","on_interval","maximum_of","function"]:pblID, |
36 (["DiffAppl","on_interval","maximum_of","function"]:pblID, |
41 ]), |
41 ]), |
42 |
42 |
43 prep_pbt DiffAppl.thy |
43 prep_pbt DiffAppl.thy |
44 (["DiffAppl","find_values","tool"]:pblID, |
44 (["DiffAppl","find_values","tool"]:pblID, |
45 [("#Given" ,"maxArgument ma_"), |
45 [("#Given" ,"maxArgument ma_"), |
46 ("#Given" ,"functionTerm f_"), |
46 ("#Given" ,"functionTerm f_f"), |
47 ("#Given" ,"boundVariable v_v"), |
47 ("#Given" ,"boundVariable v_v"), |
48 ("#Find" ,"valuesFor vls_"), |
48 ("#Find" ,"valuesFor vls_"), |
49 ("#Relate","additionalRels rs_") |
49 ("#Relate","additionalRels rs_") |
50 ]) |
50 ]) |
51 ]); |
51 ]); |
66 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
66 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
67 scr=EmptyScr} : met), |
67 scr=EmptyScr} : met), |
68 |
68 |
69 (("DiffAppl","make_fun_by_new_variable"):metID, |
69 (("DiffAppl","make_fun_by_new_variable"):metID, |
70 {ppc = prep_met DiffAppl.thy |
70 {ppc = prep_met DiffAppl.thy |
71 [("#Given" ,"functionOf f_"), |
71 [("#Given" ,"functionOf f_f"), |
72 ("#Given" ,"boundVariable v_v"), |
72 ("#Given" ,"boundVariable v_v"), |
73 ("#Given" ,"equalities eqs_"), |
73 ("#Given" ,"equalities eqs"), |
74 ("#Find" ,"functionTerm f_0_") |
74 ("#Find" ,"functionTerm f_0_") |
75 ], |
75 ], |
76 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
76 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
77 scr=EmptyScr} : met), |
77 scr=EmptyScr} : met), |
78 |
78 |
79 (("DiffAppl","make_fun_by_explicit"):metID, |
79 (("DiffAppl","make_fun_by_explicit"):metID, |
80 {ppc = prep_met DiffAppl.thy |
80 {ppc = prep_met DiffAppl.thy |
81 [("#Given" ,"functionOf f_"), |
81 [("#Given" ,"functionOf f_f"), |
82 ("#Given" ,"boundVariable v_v"), |
82 ("#Given" ,"boundVariable v_v"), |
83 ("#Given" ,"equalities eqs_"), |
83 ("#Given" ,"equalities eqs"), |
84 ("#Find" ,"functionTerm f_0_") |
84 ("#Find" ,"functionTerm f_0_") |
85 ], |
85 ], |
86 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
86 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
87 scr=EmptyScr} : met), |
87 scr=EmptyScr} : met), |
88 |
88 |