1.1 --- a/test/Tools/isac/Knowledge/integrate.thy	Thu Sep 26 17:47:10 2019 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/integrate.thy	Tue Oct 01 10:47:25 2019 +0200
     1.3 @@ -11,20 +11,15 @@
     1.4  partial_function (tailrec) integration_test :: "real \<Rightarrow> real \<Rightarrow> real"
     1.5    where
     1.6  "integration_test f_f v_v =
     1.7 -  (((Rewrite_Set_Inst [(''bdv'',v_v)] ''integration_rules'' False) @@
     1.8 -    (Rewrite_Set_Inst [(''bdv'',v_v)] ''add_new_c'' False)         @@
     1.9 -    (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'' False)) (f_f::real))"
    1.10 +  (((Rewrite_Set_Inst [(''bdv'',v_v)] ''integration_rules'') @@
    1.11 +    (Rewrite_Set_Inst [(''bdv'',v_v)] ''add_new_c'')         @@
    1.12 +    (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'')) (f_f::real))"
    1.13  setup \<open>KEStore_Elems.add_mets
    1.14    [Specify.prep_met @{theory "Isac_Knowledge"} "met_testint" [] Celem.e_metID
    1.15  	    (["diff","integration","test"],
    1.16  	      [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find", ["antiDerivative F_F"])],
    1.17  	      {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
    1.18  	        crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
    1.19 -	      @{thm integration_test.simps}
    1.20 -	    (*"Program IntegrationScript (f_f::real) (v_v::real) =             \
    1.21 -  	      \  (((Rewrite_Set_Inst [(''bdv'',v_v)] ''integration_rules'' False) @@ \
    1.22 -          \    (Rewrite_Set_Inst [(''bdv'',v_v)] ''add_new_c'' False)         @@ \
    1.23 -          \    (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'' False)) (f_f::real))"*))]
    1.24 -\<close>
    1.25 +	      @{thm integration_test.simps})]\<close>
    1.26  
    1.27  end