equal
deleted
inserted
replaced
29 "--------------------------------------------------------"; |
29 "--------------------------------------------------------"; |
30 "--------------------------------------------------------"; |
30 "--------------------------------------------------------"; |
31 "--------------------------------------------------------"; |
31 "--------------------------------------------------------"; |
32 |
32 |
33 val thy = @{theory "PolyMinus"}; |
33 val thy = @{theory "PolyMinus"}; |
|
34 val ctxt = Proof_Context.init_global thy; |
34 |
35 |
35 "----------- fun identifier --------------------------------------------------------------------"; |
36 "----------- fun identifier --------------------------------------------------------------------"; |
36 "----------- fun identifier --------------------------------------------------------------------"; |
37 "----------- fun identifier --------------------------------------------------------------------"; |
37 "----------- fun identifier --------------------------------------------------------------------"; |
38 "----------- fun identifier --------------------------------------------------------------------"; |
38 if identifier (TermC.str2term "12 ::real") = "12" then () else error "identifier 1"; |
39 if identifier (TermC.str2term "12 ::real") = "12" then () else error "identifier 1"; |
339 val str = |
340 val str = |
340 "Program SimplifyScript (t_t::real) = \ |
341 "Program SimplifyScript (t_t::real) = \ |
341 \ (((Try (Rewrite_Set ordne_alphabetisch False)) #> \ |
342 \ (((Try (Rewrite_Set ordne_alphabetisch False)) #> \ |
342 \ (Try (Rewrite_Set fasse_zusammen False)) #> \ |
343 \ (Try (Rewrite_Set fasse_zusammen False)) #> \ |
343 \ (Try (Rewrite_Set verschoenere False))) t_t)" |
344 \ (Try (Rewrite_Set verschoenere False))) t_t)" |
344 val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str; |
345 val sc = (inst_abs o (TermC.parseNEW' ctxt)) str; |
345 TermC.atomty sc; |
346 TermC.atomty sc; |
346 |
347 |
347 "----------- me simplification.for_polynomials.with_minus"; |
348 "----------- me simplification.for_polynomials.with_minus"; |
348 "----------- me simplification.for_polynomials.with_minus"; |
349 "----------- me simplification.for_polynomials.with_minus"; |
349 "----------- me simplification.for_polynomials.with_minus"; |
350 "----------- me simplification.for_polynomials.with_minus"; |
446 \ (let e_e = Take e_e; \ |
447 \ (let e_e = Take e_e; \ |
447 \ e_e = Substitute w_s e_e \ |
448 \ e_e = Substitute w_s e_e \ |
448 \ in (Repeat((Try (Repeat (Calculate ''TIMES''))) #> \ |
449 \ in (Repeat((Try (Repeat (Calculate ''TIMES''))) #> \ |
449 \ (Try (Repeat (Calculate ''PLUS''))) #> \ |
450 \ (Try (Repeat (Calculate ''PLUS''))) #> \ |
450 \ (Try (Repeat (Calculate ''MINUS''))))) e_e)" |
451 \ (Try (Repeat (Calculate ''MINUS''))))) e_e)" |
451 val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str; |
452 val sc = (inst_abs o (TermC.parseNEW' ctxt)) str; |
452 TermC.atomty sc; |
453 TermC.atomty sc; |
453 |
454 |
454 "----------- pbl polynom probe -----------------------------------"; |
455 "----------- pbl polynom probe -----------------------------------"; |
455 "----------- pbl polynom probe -----------------------------------"; |
456 "----------- pbl polynom probe -----------------------------------"; |
456 "----------- pbl polynom probe -----------------------------------"; |
457 "----------- pbl polynom probe -----------------------------------"; |