1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Tue May 19 12:33:35 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Wed May 20 12:52:09 2020 +0200
     1.3 @@ -332,20 +332,20 @@
     1.4  (** problems **)
     1.5  setup \<open>KEStore_Elems.add_pbts
     1.6    [(Problem.prep_input thy "pbl_fun_integ" [] Problem.id_empty
     1.7 -      (["integrate","function"],
     1.8 +      (["integrate", "function"],
     1.9          [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
    1.10            ("#Find"  ,["antiDerivative F_F"])],
    1.11          Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], 
    1.12          SOME "Integrate (f_f, v_v)", 
    1.13 -        [["diff","integration"]])),
    1.14 +        [["diff", "integration"]])),
    1.15      (*here "named" is used differently from Differentiation"*)
    1.16      (Problem.prep_input thy "pbl_fun_integ_nam" [] Problem.id_empty
    1.17 -      (["named","integrate","function"],
    1.18 +      (["named", "integrate", "function"],
    1.19          [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
    1.20            ("#Find"  ,["antiDerivativeName F_F"])],
    1.21          Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], 
    1.22          SOME "Integrate (f_f, v_v)", 
    1.23 -        [["diff","integration","named"]]))]\<close>
    1.24 +        [["diff", "integration", "named"]]))]\<close>
    1.25  
    1.26  (** methods **)
    1.27  
    1.28 @@ -358,7 +358,7 @@
    1.29      (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'') t_t)"
    1.30  setup \<open>KEStore_Elems.add_mets
    1.31      [Method.prep_input thy "met_diffint" [] Method.id_empty
    1.32 -	    (["diff","integration"],
    1.33 +	    (["diff", "integration"],
    1.34  	      [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find"  ,["antiDerivative F_F"])],
    1.35  	      {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
    1.36  	        crls = Atools_erls, errpats = [], nrls = Rule_Set.empty},
    1.37 @@ -376,7 +376,7 @@
    1.38      ) t_t)"
    1.39  setup \<open>KEStore_Elems.add_mets
    1.40      [Method.prep_input thy "met_diffint_named" [] Method.id_empty
    1.41 -	    (["diff","integration","named"],
    1.42 +	    (["diff", "integration", "named"],
    1.43  	      [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
    1.44  	        ("#Find"  ,["antiDerivativeName F_F"])],
    1.45  	      {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,