test/Tools/isac/Knowledge/diffapp.sml
branchdecompose-isar
changeset 42203 8e216c5001bd
parent 42195 ac2c5fb8fedd
child 42204 b6c894902413
     1.1 --- a/test/Tools/isac/Knowledge/diffapp.sml	Tue Jul 26 13:30:37 2011 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml	Tue Jul 26 15:25:28 2011 +0200
     1.3 @@ -455,25 +455,25 @@
     1.4  *)
     1.5  
     1.6  
     1.7 -(*=== inhibit exn 110722=============================================================
     1.8  
     1.9  "--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------";
    1.10  "--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------";
    1.11  "--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------";
    1.12  str2term
    1.13 -  "Script Maximum_value(f_ix::bool list)(m_::real) (r_s::bool list)\
    1.14 -   \      (v_v::real) (itv_v::real set) (err_::bool) =          \ 
    1.15 -   \ (let e_e = (hd o (filterVar m_)) r_s;              \
    1.16 -   \      t_ = (if 1 < length_ r_s                            \
    1.17 -   \           then (SubProblem (Reals_,[make,function],[no_met])\
    1.18 -   \                     [REAL m_, REAL v_v, BOOL_LIST r_s])\
    1.19 +  "Script Maximum_value(f_ix::bool list)(m_m::real) (r_s::bool list)\
    1.20 +   \      (v_v::real) (itv_v::real set) (err_r::bool) =          \ 
    1.21 +   \ (let e_e = (hd o (filterVar m_m)) r_s;              \
    1.22 +   \      t_t = (if 1 < length_h r_s                            \
    1.23 +   \           then (SubProblem (Reals_s,[make,function],[no_met])\
    1.24 +   \                     [REAL m_m, REAL v_v, BOOL_LIST r_s])\
    1.25     \           else (hd r_s));                                \
    1.26 -   \      (mx_::real) = SubProblem (Reals_,[on_interval,max_of,function], \
    1.27 +   \      (mx_x::real) = SubProblem (Reals_s,[on_interval,max_of,function], \
    1.28     \                                [Isac,maximum_on_interval])\
    1.29 -   \                               [BOOL t_, REAL v_v, REAL_SET itv_]\
    1.30 -   \ in ((SubProblem (Reals_,[find_values,tool],[Isac,find_values])   \
    1.31 -   \      [REAL mx_, REAL (Rhs t_), REAL v_v, REAL m_,     \
    1.32 +   \                               [BOOL t_t, REAL v_v, REAL_SET itv_v]\
    1.33 +   \ in ((SubProblem (Reals_s,[find_values,tool],[Isac,find_values])   \
    1.34 +   \      [REAL mx_x, REAL (Rhs t_t), REAL v_v, REAL m_m,     \
    1.35     \       BOOL_LIST (dropWhile (ident e_e) r_s)])::bool list))";
    1.36 +(*=== inhibit exn 110722=============================================================
    1.37  
    1.38  val f_ix = (str2term "f_ix::bool list", 
    1.39  	    str2term "[r=Arbfix]");
    1.40 @@ -768,3 +768,4 @@
    1.41  
    1.42  ===== inhibit exn 110722===========================================================*)
    1.43  
    1.44 +