1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Sat Jun 22 13:15:52 2019 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Sat Jun 22 14:34:06 2019 +0200
     1.3 @@ -20,12 +20,6 @@
     1.4    (*the CAS-command, eg. "Integrate (2*x^^^3, x)"*)
     1.5    Integrate           :: "[real * real] => real"
     1.6  
     1.7 -  (*Script-names*)
     1.8 -  IntegrationScript      :: "[real,real,  real] => real"
     1.9 -                  ("((Script IntegrationScript (_ _ =))// (_))" 9)
    1.10 -  NamedIntegrationScript :: "[real,real, real=>real,  bool] => bool"
    1.11 -                  ("((Script NamedIntegrationScript (_ _ _=))// (_))" 9)
    1.12 -
    1.13  axiomatization where
    1.14  (*stated as axioms, todo: prove as theorems
    1.15    'bdv' is a constant handled on the meta-level 
    1.16 @@ -367,10 +361,7 @@
    1.17  	      [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find"  ,["antiDerivative F_F"])],
    1.18  	      {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
    1.19  	        crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
    1.20 -	      @{thm integrate.simps}
    1.21 -	    (*"Script IntegrationScript (f_f::real) (v_v::real) =                " ^
    1.22 -          "  (let t_t = Take (Integral f_f D v_v)                             " ^
    1.23 -          "   in (Rewrite_Set_Inst [(''bdv'',v_v)] ''integration'' False) (t_t::real))"*))]
    1.24 +	      @{thm integrate.simps})]
    1.25  \<close>
    1.26  
    1.27  partial_function (tailrec) intergrate_named :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool"
    1.28 @@ -385,11 +376,7 @@
    1.29  	        ("#Find"  ,["antiDerivativeName F_F"])],
    1.30  	      {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
    1.31            crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
    1.32 -        @{thm intergrate_named.simps}
    1.33 -	    (*"Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = " ^
    1.34 -          "  (let t_t = Take (F_F v_v = Integral f_f D v_v)                            " ^
    1.35 -          "   in ((Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'' False)) @@  " ^
    1.36 -          "       (Rewrite_Set_Inst [(''bdv'',v_v)] ''integration'' False)) t_t)            "*))]
    1.37 +        @{thm intergrate_named.simps})]
    1.38  \<close>
    1.39  
    1.40  end
    1.41 \ No newline at end of file