1.1 --- a/src/Tools/isac/Knowledge/Diff.thy	Wed Dec 14 14:20:25 2016 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Diff.thy	Sun Dec 18 16:27:41 2016 +0100
     1.3 @@ -248,8 +248,8 @@
     1.4  
     1.5  (** problem types **)
     1.6  setup {* KEStore_Elems.add_pbts
     1.7 -  [(prep_pbt thy "pbl_fun" [] e_pblID (["function"], [], e_rls, NONE, [])),
     1.8 -    (prep_pbt thy "pbl_fun_deriv" [] e_pblID
     1.9 +  [(Specify.prep_pbt thy "pbl_fun" [] e_pblID (["function"], [], e_rls, NONE, [])),
    1.10 +    (Specify.prep_pbt thy "pbl_fun_deriv" [] e_pblID
    1.11        (["derivative_of","function"],
    1.12          [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
    1.13            ("#Find"  ,["derivative f_f'"])],
    1.14 @@ -257,7 +257,7 @@
    1.15          SOME "Diff (f_f, v_v)", [["diff","differentiate_on_R"],
    1.16  			  ["diff","after_simplification"]])),
    1.17      (*here "named" is used differently from Integration"*)
    1.18 -    (prep_pbt thy "pbl_fun_deriv_nam" [] e_pblID
    1.19 +    (Specify.prep_pbt thy "pbl_fun_deriv_nam" [] e_pblID
    1.20        (["named","derivative_of","function"],
    1.21          [("#Given" ,["functionEq f_f","differentiateFor v_v"]),
    1.22            ("#Find"  ,["derivativeEq f_f'"])],
    1.23 @@ -281,12 +281,12 @@
    1.24    | argl2dtss _ = error "Diff.ML: wrong argument for argl2dtss";
    1.25  *}
    1.26  setup {* KEStore_Elems.add_mets
    1.27 -  [prep_met thy "met_diff" [] e_metID
    1.28 +  [Specify.prep_met thy "met_diff" [] e_metID
    1.29        (["diff"], [],
    1.30          {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
    1.31            crls = Atools_erls, errpats = [], nrls = norm_diff},
    1.32          "empty_script"),
    1.33 -    prep_met thy "met_diff_onR" [] e_metID
    1.34 +    Specify.prep_met thy "met_diff_onR" [] e_metID
    1.35        (["diff","differentiate_on_R"],
    1.36          [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
    1.37            ("#Find"  ,["derivative f_f'"])],
    1.38 @@ -314,7 +314,7 @@
    1.39            "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var        False)) Or " ^
    1.40            "    (Repeat (Rewrite_Set             make_polynomial False)))) @@ " ^
    1.41            " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f')"),
    1.42 -    prep_met thy "met_diff_simpl" [] e_metID
    1.43 +    Specify.prep_met thy "met_diff_simpl" [] e_metID
    1.44        (["diff","diff_simpl"],
    1.45          [("#Given", ["functionTerm f_f","differentiateFor v_v"]),
    1.46           ("#Find" , ["derivative f_f'"])],
    1.47 @@ -342,7 +342,7 @@
    1.48            "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var        False)) Or " ^
    1.49            "    (Repeat (Rewrite_Set              make_polynomial False))))  " ^
    1.50            " )) f_f')"),
    1.51 -    prep_met thy "met_diff_equ" [] e_metID
    1.52 +    Specify.prep_met thy "met_diff_equ" [] e_metID
    1.53        (["diff","differentiate_equality"],
    1.54          [("#Given" ,["functionEq f_f","differentiateFor v_v"]),
    1.55            ("#Find"  ,["derivativeEq f_f'"])],
    1.56 @@ -371,7 +371,7 @@
    1.57            "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var        False)) Or   " ^
    1.58            "    (Repeat (Rewrite_Set             make_polynomial False)))) @@ " ^
    1.59            " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f')"),
    1.60 -    prep_met thy "met_diff_after_simp" [] e_metID
    1.61 +    Specify.prep_met thy "met_diff_after_simp" [] e_metID
    1.62        (["diff","after_simplification"],
    1.63          [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
    1.64            ("#Find"  ,["derivative f_f'"])],