equal
deleted
inserted
replaced
374 |
374 |
375 "----------- check Scripts ------------------------------"; |
375 "----------- check Scripts ------------------------------"; |
376 "----------- check Scripts ------------------------------"; |
376 "----------- check Scripts ------------------------------"; |
377 "----------- check Scripts ------------------------------"; |
377 "----------- check Scripts ------------------------------"; |
378 val str = |
378 val str = |
379 "Script IntegrationScript (f_f::real) (v_v::real) = \ |
379 "Program IntegrationScript (f_f::real) (v_v::real) = \ |
380 \ (let t_t = Take (Integral f_f D v_v) \ |
380 \ (let t_t = Take (Integral f_f D v_v) \ |
381 \ in (Rewrite_Set_Inst [(''bdv'',v_v)] integration False) (t_t::real))"; |
381 \ in (Rewrite_Set_Inst [(''bdv'',v_v)] integration False) (t_t::real))"; |
382 val sc = (inst_abs o Thm.term_of o the o (parse thy)) str; |
382 val sc = (inst_abs o Thm.term_of o the o (parse thy)) str; |
383 atomty sc; |
383 atomty sc; |
384 |
384 |
385 val str = |
385 val str = |
386 "Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = \ |
386 "Program NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = \ |
387 \ (let t_t = Take (F_F v_v = Integral f_f D v_v) \ |
387 \ (let t_t = Take (F_F v_v = Integral f_f D v_v) \ |
388 \ in (Rewrite_Set_Inst [(''bdv'',v_v)] integration False) t_t)"; |
388 \ in (Rewrite_Set_Inst [(''bdv'',v_v)] integration False) t_t)"; |
389 val sc = (inst_abs o Thm.term_of o the o (parse thy)) str; |
389 val sc = (inst_abs o Thm.term_of o the o (parse thy)) str; |
390 atomty sc; |
390 atomty sc; |
391 show_mets(); |
391 show_mets(); |