src/Tools/isac/Knowledge/RatEq.thy
branchisac-update-Isa09-2
changeset 37984 972a73d7c50b
parent 37983 03bfbc480107
child 37988 03e6d5db883e
equal deleted inserted replaced
37983:03bfbc480107 37984:972a73d7c50b
   207     "(let e_e = ((Repeat(Try (Rewrite_Set RatEq_simplify      True))) @@  " ^
   207     "(let e_e = ((Repeat(Try (Rewrite_Set RatEq_simplify      True))) @@  " ^
   208     "           (Repeat(Try (Rewrite_Set norm_Rational      False))) @@  " ^
   208     "           (Repeat(Try (Rewrite_Set norm_Rational      False))) @@  " ^
   209     "           (Repeat(Try (Rewrite_Set common_nominator_p False))) @@  " ^
   209     "           (Repeat(Try (Rewrite_Set common_nominator_p False))) @@  " ^
   210     "           (Repeat(Try (Rewrite_Set RatEq_eliminate     True)))) e_;" ^
   210     "           (Repeat(Try (Rewrite_Set RatEq_eliminate     True)))) e_;" ^
   211     " (L_::bool list) =  (SubProblem (RatEq_,[univariate,equation],      " ^
   211     " (L_::bool list) =  (SubProblem (RatEq_,[univariate,equation],      " ^
   212     "                [no_met]) [bool_ e_e, real_ v_])                     " ^
   212     "                [no_met]) [BOOL e_e, REAL v_])                     " ^
   213     " in Check_elementwise L_ {(v_v::real). Assumptions})"
   213     " in Check_elementwise L_ {(v_v::real). Assumptions})"
   214    ));
   214    ));
   215 
   215 
   216 calclist':= overwritel (!calclist', 
   216 calclist':= overwritel (!calclist', 
   217    [("is_ratequation_in", ("RatEq.is_ratequation_in", 
   217    [("is_ratequation_in", ("RatEq.is_ratequation_in",