6 theory' := overwritel (!theory', [("DiffAppl.thy",DiffAppl.thy)]);
9 > get_pbt ["DiffAppl.thy","maximum_of","function"];
10 > get_met ("Script.thy","max_on_interval_by_calculus");
13 pbltypes:= overwritel (!pbltypes,
16 (["DiffAppl.thy","maximum_of","function"],
17 [("#Given" ,"fixedValues fix_"),
18 ("#Find" ,"maximum m_"),
19 ("#Find" ,"valuesFor vs_"),
20 ("#Relate","relations rs_") (*,
21 ("#where" ,"foldl (op&) True (map (Not o ((op<=) #0) o Rhs) fix_)"),
22 ("#with" ,"Ex_frees ((foldl (op &) True rs_) & \
23 \ (ALL m'. (subst (m_,m') (foldl (op &) True rs_) \
24 \ --> m' <= m_)))") *)
28 (["DiffAppl.thy","make","function"]:pblID,
29 [("#Given" ,"functionOf f_"),
30 ("#Given" ,"boundVariable v_"),
31 ("#Given" ,"equalities eqs_"),
32 ("#Find" ,"functionTerm f_0_")
36 (["DiffAppl.thy","on_interval","maximum_of","function"]:pblID,
37 [("#Given" ,"functionTerm t_"),
38 ("#Given" ,"boundVariable v_"),
39 ("#Given" ,"interval itv_"),
40 ("#Find" ,"maxArgument v_0_")
44 (["DiffAppl.thy","find_values","tool"]:pblID,
45 [("#Given" ,"maxArgument ma_"),
46 ("#Given" ,"functionTerm f_"),
47 ("#Given" ,"boundVariable v_"),
48 ("#Find" ,"valuesFor vls_"),
49 ("#Relate","additionalRels rs_")
54 methods:= overwritel (!methods,
56 (("DiffAppl.thy","max_by_calculus"):metID,
57 {ppc = prep_met DiffAppl.thy
58 [("#Given" ,"fixedValues fix_"),
59 ("#Given" ,"boundVariable v_"),
60 ("#Given" ,"interval itv_"),
61 ("#Given" ,"errorBound err_"),
62 ("#Find" ,"maximum m_"),
63 ("#Find" ,"valuesFor vs_"),
64 ("#Relate","relations rs_")
66 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
69 (("DiffAppl.thy","make_fun_by_new_variable"):metID,
70 {ppc = prep_met DiffAppl.thy
71 [("#Given" ,"functionOf f_"),
72 ("#Given" ,"boundVariable v_"),
73 ("#Given" ,"equalities eqs_"),
74 ("#Find" ,"functionTerm f_0_")
76 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
79 (("DiffAppl.thy","make_fun_by_explicit"):metID,
80 {ppc = prep_met DiffAppl.thy
81 [("#Given" ,"functionOf f_"),
82 ("#Given" ,"boundVariable v_"),
83 ("#Given" ,"equalities eqs_"),
84 ("#Find" ,"functionTerm f_0_")
86 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
89 (("DiffAppl.thy","max_on_interval_by_calculus"):metID,
90 {ppc = prep_met DiffAppl.thy
91 [("#Given" ,"functionTerm t_"),
92 ("#Given" ,"boundVariable v_"),
93 ("#Given" ,"interval itv_"),
94 ("#Given" ,"errorBound err_"),
95 ("#Find" ,"maxArgument v_0_")
97 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
100 (("DiffAppl.thy","find_values"):metID,
101 {ppc = prep_met DiffAppl.thy
103 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],