src/Tools/isac/Knowledge/DiffApp.thy
branchisac-update-Isa09-2
changeset 37991 028442673981
parent 37984 972a73d7c50b
child 37994 eb4c556a525b
equal deleted inserted replaced
37990:24609758d219 37991:028442673981
   160     ],
   160     ],
   161   {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls,
   161   {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls,
   162     crls = eval_rls, nrls=norm_Rational
   162     crls = eval_rls, nrls=norm_Rational
   163    (*,  asm_rls=[],asm_thm=[]*)},
   163    (*,  asm_rls=[],asm_thm=[]*)},
   164   "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)       " ^
   164   "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)       " ^
   165   "      (v_v::real) (itv_::real set) (err_::bool) =                       " ^ 
   165   "      (v_v::real) (itv_v::real set) (err_::bool) =                       " ^ 
   166   " (let e_e = (hd o (filterVar m_)) rs_;                                  " ^
   166   " (let e_e = (hd o (filterVar m_)) rs_;                                  " ^
   167   "      t_ = (if 1 < length_ rs_                                         " ^
   167   "      t_ = (if 1 < length_ rs_                                         " ^
   168   "           then (SubProblem (DiffApp_,[make,function],[no_met])        " ^
   168   "           then (SubProblem (DiffApp_,[make,function],[no_met])        " ^
   169   "                     [REAL m_, REAL v_v, BOOL_LIST rs_])             " ^
   169   "                     [REAL m_, REAL v_v, BOOL_LIST rs_])             " ^
   170   "           else (hd rs_));                                             " ^
   170   "           else (hd rs_));                                             " ^