equal
deleted
inserted
replaced
151 ], |
151 ], |
152 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], |
152 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], |
153 srls = e_rls, |
153 srls = e_rls, |
154 prls=e_rls, |
154 prls=e_rls, |
155 crls = Atools_erls, nrls = e_rls}, |
155 crls = Atools_erls, nrls = e_rls}, |
156 "Script IntegrationScript (f_::real) (v_::real) = \ |
156 "Script IntegrationScript (f_::real) (v_::real) = \ |
157 \ ((Rewrite_Set_Inst [(bdv,v_)] integration_rules False)\ |
157 \ (let t_ = Integral f_ D v_ \ |
158 \ (Integral f_ D v_))" |
158 \ in (Rewrite_Set_Inst [(bdv,v_)] integration False) (t_::real))" |
159 )); |
159 )); |
160 |
160 |
161 store_met |
161 store_met |
162 (prep_met Integrate.thy |
162 (prep_met Integrate.thy |
163 (["Diff","integration","named"], |
163 (["Diff","integration","named"], |
166 ], |
166 ], |
167 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], |
167 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], |
168 srls = e_rls, |
168 srls = e_rls, |
169 prls=e_rls, |
169 prls=e_rls, |
170 crls = Atools_erls, nrls = e_rls}, |
170 crls = Atools_erls, nrls = e_rls}, |
171 "Script NamedIntegrationScript (f_::real) (v_::real) (F_::real) = \ |
171 "Script NamedIntegrationScript (f_::real) (v_::real) (F_::real) = \ |
172 \ (F_ = Integral f_ D v_)" |
172 \ (let t_ = (F_ = Integral f_ D v_) \ |
|
173 \ in (Rewrite_Set_Inst [(bdv,v_)] integration False) t_)" |
173 )); |
174 )); |
174 |
175 |