src/Tools/isac/Knowledge/RatEq.thy
changeset 52105 2786cc9704c8
parent 48789 498ed5bb1004
child 52125 6f1d3415dc68
equal deleted inserted replaced
52104:83166e7c7e52 52105:2786cc9704c8
   219     calc=[],
   219     calc=[],
   220     crls=RatEq_crls, errpats = [], nrls = norm_Rational},
   220     crls=RatEq_crls, errpats = [], nrls = norm_Rational},
   221    "Script Solve_rat_equation  (e_e::bool) (v_v::real) =                   " ^
   221    "Script Solve_rat_equation  (e_e::bool) (v_v::real) =                   " ^
   222     "(let e_e = ((Repeat(Try (Rewrite_Set RatEq_simplify      True))) @@  " ^
   222     "(let e_e = ((Repeat(Try (Rewrite_Set RatEq_simplify      True))) @@  " ^
   223     "           (Repeat(Try (Rewrite_Set norm_Rational      False))) @@  " ^
   223     "           (Repeat(Try (Rewrite_Set norm_Rational      False))) @@  " ^
   224     "           (Repeat(Try (Rewrite_Set common_nominator_p False))) @@  " ^
   224     "           (Repeat(Try (Rewrite_Set add_fractions_p False))) @@  " ^
   225     "           (Repeat(Try (Rewrite_Set RatEq_eliminate     True)))) e_e;" ^
   225     "           (Repeat(Try (Rewrite_Set RatEq_eliminate     True)))) e_e;" ^
   226     " (L_L::bool list) = (SubProblem (RatEq',[univariate,equation], [no_met])" ^
   226     " (L_L::bool list) = (SubProblem (RatEq',[univariate,equation], [no_met])" ^
   227     "                    [BOOL e_e, REAL v_v])                     " ^
   227     "                    [BOOL e_e, REAL v_v])                     " ^
   228     " in Check_elementwise L_L {(v_v::real). Assumptions})"
   228     " in Check_elementwise L_L {(v_v::real). Assumptions})"
   229    ));
   229    ));