equal
deleted
inserted
replaced
484 |
484 |
485 (*GoOn.5.03. script with Map, Subst (biquadr.equ.) |
485 (*GoOn.5.03. script with Map, Subst (biquadr.equ.) |
486 val scr = Prog ((inst_abs o Thm.term_of o the o (parse thy)) |
486 val scr = Prog ((inst_abs o Thm.term_of o the o (parse thy)) |
487 "Script Biquadrat_poly (e_e::bool) (v_::real) = \ |
487 "Script Biquadrat_poly (e_e::bool) (v_::real) = \ |
488 \(let e_e = Substitute [(v_^^^4, v_0_^^^2),(v_^^^2, v_0_)] e_; \ |
488 \(let e_e = Substitute [(v_^^^4, v_0_^^^2),(v_^^^2, v_0_)] e_; \ |
489 \ L_0_ = (SubProblem (PolyEq_,[univariate,equation], [no_met]) \ |
489 \ L_0_ = (SubProblem (PolyEqX,[univariate,equation], [no_met]) \ |
490 \ [BOOL e_e, REAL v_0_]); \ |
490 \ [BOOL e_e, REAL v_0_]); \ |
491 \ L_i_ = Map (((Substitute [(v_0_, v_^^^2)]) @@ \ |
491 \ L_i_ = Map (((Substitute [(v_0_, v_^^^2)]) @@ \ |
492 \ ((Rewrite real_root_positive False) Or \ |
492 \ ((Rewrite real_root_positive False) Or \ |
493 \ (Rewrite real_root_negative False)) @@ \ |
493 \ (Rewrite real_root_negative False)) @@ \ |
494 \ OrToList) L_0_ \ |
494 \ OrToList) L_0_ \ |