1.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Wed Sep 08 17:17:29 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Wed Sep 08 17:20:03 2010 +0200
1.3 @@ -96,21 +96,21 @@
1.4 store_pbt
1.5 (prep_pbt thy "pbl_fun_make" [] e_pblID
1.6 (["make","function"]:pblID,
1.7 - [("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]),
1.8 + [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
1.9 ("#Find" ,["functionEq f_1_"])
1.10 ],
1.11 e_rls, NONE, []));
1.12 store_pbt
1.13 (prep_pbt thy "pbl_fun_max_expl" [] e_pblID
1.14 (["by_explicit","make","function"]:pblID,
1.15 - [("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]),
1.16 + [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
1.17 ("#Find" ,["functionEq f_1_"])
1.18 ],
1.19 e_rls, NONE, [["DiffApp","make_fun_by_explicit"]]));
1.20 store_pbt
1.21 (prep_pbt thy "pbl_fun_max_newvar" [] e_pblID
1.22 (["by_new_variable","make","function"]:pblID,
1.23 - [("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]),
1.24 + [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
1.25 (*WN.12.5.03: precond for distinction still missing*)
1.26 ("#Find" ,["functionEq f_1_"])
1.27 ],
1.28 @@ -134,7 +134,7 @@
1.29 store_pbt
1.30 (prep_pbt thy "pbl_tool_findvals" [] e_pblID
1.31 (["find_values","tool"]:pblID,
1.32 - [("#Given" ,["maxArgument ma_","functionEq f_","boundVariable v_v"]),
1.33 + [("#Given" ,["maxArgument ma_","functionEq f_f","boundVariable v_v"]),
1.34 ("#Find" ,["valuesFor vls_"]),
1.35 ("#Relate",["additionalRels rs_"])
1.36 ],
1.37 @@ -179,15 +179,15 @@
1.38 store_met
1.39 (prep_met thy "met_diffapp_funnew" [] e_metID
1.40 (["DiffApp","make_fun_by_new_variable"]:metID,
1.41 - [("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]),
1.42 + [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
1.43 ("#Find" ,["functionEq f_1_"])
1.44 ],
1.45 {rew_ord'="tless_true",rls'=eval_rls,srls=list_rls,prls=e_rls,
1.46 calc=[], crls = eval_rls, nrls=norm_Rational(*,asm_rls=[],asm_thm=[]*)},
1.47 - "Script Make_fun_by_new_variable (f_::real) (v_v::real) " ^
1.48 - " (eqs_::bool list) = " ^
1.49 - "(let h_ = (hd o (filterVar f_)) eqs_; " ^
1.50 - " es_ = dropWhile (ident h_) eqs_; " ^
1.51 + "Script Make_fun_by_new_variable (f_f::real) (v_v::real) " ^
1.52 + " (eqs::bool list) = " ^
1.53 + "(let h_ = (hd o (filterVar f_)) eqs; " ^
1.54 + " es_ = dropWhile (ident h_) eqs; " ^
1.55 " vs_ = dropWhile (ident f_) (Vars h_); " ^
1.56 " v_1 = nth_ 1 vs_; " ^
1.57 " v_2 = nth_ 2 vs_; " ^
1.58 @@ -204,16 +204,16 @@
1.59 store_met
1.60 (prep_met thy "met_diffapp_funexp" [] e_metID
1.61 (["DiffApp","make_fun_by_explicit"]:metID,
1.62 - [("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]),
1.63 + [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
1.64 ("#Find" ,["functionEq f_1_"])
1.65 ],
1.66 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls,
1.67 crls = eval_rls, nrls=norm_Rational
1.68 (*, asm_rls=[],asm_thm=[]*)},
1.69 - "Script Make_fun_by_explicit (f_::real) (v_v::real) " ^
1.70 - " (eqs_::bool list) = " ^
1.71 - " (let h_ = (hd o (filterVar f_)) eqs_; " ^
1.72 - " e_1 = hd (dropWhile (ident h_) eqs_); " ^
1.73 + "Script Make_fun_by_explicit (f_f::real) (v_v::real) " ^
1.74 + " (eqs::bool list) = " ^
1.75 + " (let h_ = (hd o (filterVar f_)) eqs; " ^
1.76 + " e_1 = hd (dropWhile (ident h_) eqs); " ^
1.77 " vs_ = dropWhile (ident f_) (Vars h_); " ^
1.78 " v_1 = hd (dropWhile (ident v_v) vs_); " ^
1.79 " (s_1::bool list)= " ^