src/Tools/isac/Knowledge/Integrate.thy
changeset 59637 8881c5d28f82
parent 59635 9fc1bb69813c
child 59773 d88bb023c380
     1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Wed Oct 02 15:14:51 2019 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Wed Oct 02 16:02:17 2019 +0200
     1.3 @@ -371,7 +371,7 @@
     1.4    let
     1.5      t_t = Take (F_F v_v = Integral f_f D v_v)
     1.6    in (
     1.7 -    (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''simplify_Integral'')) @@
     1.8 +    (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''simplify_Integral'')) #>
     1.9      (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'')
    1.10      ) t_t)"
    1.11  setup \<open>KEStore_Elems.add_mets