src/sml/IsacKnowledge/Integrate.ML
changeset 2918 cac1f942e1a1
parent 2917 2488337fd0dd
child 3755 c1e092099128
     1.1 --- a/src/sml/IsacKnowledge/Integrate.ML	Sat Aug 20 19:10:30 2005 +0200
     1.2 +++ b/src/sml/IsacKnowledge/Integrate.ML	Sat Aug 20 21:20:16 2005 +0200
     1.3 @@ -153,9 +153,9 @@
     1.4  		srls = e_rls, 
     1.5  		prls=e_rls,
     1.6  	     crls = Atools_erls, nrls = e_rls},
     1.7 -"Script IntegrationScript (f_::real) (v_::real) = \
     1.8 -\  ((Rewrite_Set_Inst [(bdv,v_)] integration_rules False)\
     1.9 -\    (Integral f_ D v_))"
    1.10 +"Script IntegrationScript (f_::real) (v_::real) =                \
    1.11 +\  (let t_ = Integral f_ D v_                                    \
    1.12 +\   in (Rewrite_Set_Inst [(bdv,v_)] integration False) (t_::real))"
    1.13  ));
    1.14      
    1.15  store_met
    1.16 @@ -168,7 +168,8 @@
    1.17  		srls = e_rls, 
    1.18  		prls=e_rls,
    1.19  		crls = Atools_erls, nrls = e_rls},
    1.20 - "Script NamedIntegrationScript (f_::real) (v_::real) (F_::real) = \
    1.21 -\  (F_ = Integral f_ D v_)"
    1.22 +"Script NamedIntegrationScript (f_::real) (v_::real) (F_::real) = \
    1.23 +\  (let t_ = (F_ = Integral f_ D v_)                                 \
    1.24 +\   in (Rewrite_Set_Inst [(bdv,v_)] integration False) t_)"
    1.25   ));
    1.26