1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Thu Mar 15 15:48:52 2018 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Fri Mar 23 10:14:39 2018 +0100
     1.3 @@ -342,7 +342,7 @@
     1.4        (["integrate","function"],
     1.5          [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
     1.6            ("#Find"  ,["antiDerivative F_F"])],
     1.7 -        Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)], 
     1.8 +        Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)], 
     1.9          SOME "Integrate (f_f, v_v)", 
    1.10          [["diff","integration"]])),
    1.11      (*here "named" is used differently from Differentiation"*)
    1.12 @@ -350,7 +350,7 @@
    1.13        (["named","integrate","function"],
    1.14          [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
    1.15            ("#Find"  ,["antiDerivativeName F_F"])],
    1.16 -        Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)], 
    1.17 +        Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)], 
    1.18          SOME "Integrate (f_f, v_v)", 
    1.19          [["diff","integration","named"]]))] *}
    1.20