src/Tools/isac/Knowledge/RatEq.thy
branchisac-update-Isa09-2
changeset 37991 028442673981
parent 37988 03e6d5db883e
child 38009 b49723351533
equal deleted inserted replaced
37990:24609758d219 37991:028442673981
   212     "           (Repeat(Try (Rewrite_Set norm_Rational      False))) @@  " ^
   212     "           (Repeat(Try (Rewrite_Set norm_Rational      False))) @@  " ^
   213     "           (Repeat(Try (Rewrite_Set common_nominator_p False))) @@  " ^
   213     "           (Repeat(Try (Rewrite_Set common_nominator_p False))) @@  " ^
   214     "           (Repeat(Try (Rewrite_Set RatEq_eliminate     True)))) e_e;" ^
   214     "           (Repeat(Try (Rewrite_Set RatEq_eliminate     True)))) e_e;" ^
   215     " (L_L::bool list) = (SubProblem (RatEq',[univariate,equation], [no_met])" ^
   215     " (L_L::bool list) = (SubProblem (RatEq',[univariate,equation], [no_met])" ^
   216     "                    [BOOL e_e, REAL v_v])                     " ^
   216     "                    [BOOL e_e, REAL v_v])                     " ^
   217     " in Check_elementwise L_L {(v_v::real). Assumptions})"
   217     " in Check_elementwise L_LL {(v_v::real). Assumptions})"
   218    ));
   218    ));
   219 *}
   219 *}
   220 
   220 
   221 ML {*
   221 ML {*
   222 calclist':= overwritel (!calclist', 
   222 calclist':= overwritel (!calclist',