equal
deleted
inserted
replaced
232 |
232 |
233 "----------- met simplification for_polynomials with_minus -------"; |
233 "----------- met simplification for_polynomials with_minus -------"; |
234 "----------- met simplification for_polynomials with_minus -------"; |
234 "----------- met simplification for_polynomials with_minus -------"; |
235 "----------- met simplification for_polynomials with_minus -------"; |
235 "----------- met simplification for_polynomials with_minus -------"; |
236 val str = |
236 val str = |
237 "Script SimplifyScript (t_t::real) = \ |
237 "Program SimplifyScript (t_t::real) = \ |
238 \ (((Try (Rewrite_Set ordne_alphabetisch False)) @@ \ |
238 \ (((Try (Rewrite_Set ordne_alphabetisch False)) @@ \ |
239 \ (Try (Rewrite_Set fasse_zusammen False)) @@ \ |
239 \ (Try (Rewrite_Set fasse_zusammen False)) @@ \ |
240 \ (Try (Rewrite_Set verschoenere False))) t_t)" |
240 \ (Try (Rewrite_Set verschoenere False))) t_t)" |
241 val sc = (inst_abs o Thm.term_of o the o (parse thy)) str; |
241 val sc = (inst_abs o Thm.term_of o the o (parse thy)) str; |
242 atomty sc; |
242 atomty sc; |
336 |
336 |
337 "----------- met probe fuer_polynom ------------------------------"; |
337 "----------- met probe fuer_polynom ------------------------------"; |
338 "----------- met probe fuer_polynom ------------------------------"; |
338 "----------- met probe fuer_polynom ------------------------------"; |
339 "----------- met probe fuer_polynom ------------------------------"; |
339 "----------- met probe fuer_polynom ------------------------------"; |
340 val str = |
340 val str = |
341 "Script ProbeScript (e_e::bool) (w_s::bool list) =\ |
341 "Program ProbeScript (e_e::bool) (w_s::bool list) =\ |
342 \ (let e_e = Take e_e; \ |
342 \ (let e_e = Take e_e; \ |
343 \ e_e = Substitute w_s e_e \ |
343 \ e_e = Substitute w_s e_e \ |
344 \ in (Repeat((Try (Repeat (Calculate ''TIMES''))) @@ \ |
344 \ in (Repeat((Try (Repeat (Calculate ''TIMES''))) @@ \ |
345 \ (Try (Repeat (Calculate ''PLUS''))) @@ \ |
345 \ (Try (Repeat (Calculate ''PLUS''))) @@ \ |
346 \ (Try (Repeat (Calculate ''MINUS''))))) e_e)" |
346 \ (Try (Repeat (Calculate ''MINUS''))))) e_e)" |