1.1 --- a/test/Tools/isac/OLDTESTS/script.sml Mon Sep 06 14:48:38 2010 +0200
1.2 +++ b/test/Tools/isac/OLDTESTS/script.sml Mon Sep 06 15:09:37 2010 +0200
1.3 @@ -41,17 +41,17 @@
1.4 val c = (the o (parse DiffApp.thy))
1.5 "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\
1.6 \ (v_::real) (itv_::real set) (err_::bool) = \
1.7 - \ (let e_ = (hd o (filterVar m_)) rs_; \
1.8 + \ (let e_e = (hd o (filterVar m_)) rs_; \
1.9 \ t_ = (if 1 < length_ rs_ \
1.10 \ then (SubProblem (Reals_,[make,function],[no_met])\
1.11 - \ [real_ m_, real_ v_, bool_list_ rs_])\
1.12 + \ [real_ m_, real_ v_v, bool_list_ rs_])\
1.13 \ else (hd rs_)); \
1.14 \ (mx_::real) = SubProblem (Reals_,[on_interval,max_of,function], \
1.15 \ [Isac,maximum_on_interval])\
1.16 - \ [bool_ t_, real_ v_, real_set_ itv_]\
1.17 + \ [bool_ t_, real_ v_v, real_set_ itv_]\
1.18 \ in ((SubProblem (Reals_,[find_values,tool],[Isac,find_values]) \
1.19 - \ [real_ mx_, real_ (Rhs t_), real_ v_, real_ m_, \
1.20 - \ bool_list_ (dropWhile (ident e_) rs_)])::bool list))";
1.21 + \ [real_ mx_, real_ (Rhs t_), real_ v_v, real_ m_, \
1.22 + \ bool_list_ (dropWhile (ident e_e) rs_)])::bool list))";
1.23
1.24
1.25 "################################################### 6.5.03";
1.26 @@ -147,7 +147,7 @@
1.27 \ (let h_ = (hd o (filterVar f_)) eqs_; \
1.28 \ e_1 = hd (dropWhile (ident h_) eqs_); \
1.29 \ vs_ = dropWhile (ident f_) (Vars h_); \
1.30 - \ v_1 = hd (dropWhile (ident v_) vs_); \
1.31 + \ v_1 = hd (dropWhile (ident v_v) vs_); \
1.32 \ (s_1::bool list)=(SubProblem(Reals_,[univar,equation],[no_met])\
1.33 \ [bool_ e_1, real_ v_1])\
1.34 \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)";
1.35 @@ -158,19 +158,19 @@
1.36 (*#####################################################*)
1.37 val sc = (term_of o the o (parse Test.thy))
1.38 "Script Solve_root_equation (eq_::bool) (v_::real) (err_::bool) =\
1.39 - \ (let e_ = Rewrite square_equation_left True eq_; \
1.40 - \ e_ = Rewrite_Set Test_simplify False e_; \
1.41 - \ e_ = Rewrite_Set rearrange_assoc False e_; \
1.42 - \ e_ = Rewrite_Set isolate_root False e_; \
1.43 - \ e_ = Rewrite_Set Test_simplify False e_; \
1.44 + \ (let e_e = Rewrite square_equation_left True eq_; \
1.45 + \ e_e = Rewrite_Set Test_simplify False e_; \
1.46 + \ e_e = Rewrite_Set rearrange_assoc False e_; \
1.47 + \ e_e = Rewrite_Set isolate_root False e_; \
1.48 + \ e_e = Rewrite_Set Test_simplify False e_; \
1.49
1.50 - \ e_ = Rewrite square_equation_left True e_; \
1.51 - \ e_ = Rewrite_Set Test_simplify False e_; \
1.52 + \ e_e = Rewrite square_equation_left True e_; \
1.53 + \ e_e = Rewrite_Set Test_simplify False e_; \
1.54
1.55 - \ e_ = Rewrite_Set norm_equation False e_; \
1.56 - \ e_ = Rewrite_Set Test_simplify False e_; \
1.57 - \ e_ = Rewrite_Set_Inst [(bdv,v_)] isolate_bdv False e_;\
1.58 - \ e_ = Rewrite_Set Test_simplify False e_ \
1.59 + \ e_e = Rewrite_Set norm_equation False e_; \
1.60 + \ e_e = Rewrite_Set Test_simplify False e_; \
1.61 + \ e_e = Rewrite_Set_Inst [(bdv,v_)] isolate_bdv False e_;\
1.62 + \ e_e = Rewrite_Set Test_simplify False e_e \
1.63 \ in [e_::bool])";
1.64 val ags = map (term_of o the o (parse Test.thy))
1.65 ["sqrt(#9+#4*x)=sqrt x + sqrt(#5+x)", "x::real","#0"];
1.66 @@ -250,11 +250,11 @@
1.67 val scr as (Script sc) = Script (((inst_abs Test.thy)
1.68 o term_of o the o (parse thy))
1.69 "Script Testeq (e_::bool) = \
1.70 - \(While (contains_root e_) Do \
1.71 + \(While (contains_root e_e) Do \
1.72 \((Try (Repeat (Rewrite rroot_square_inv False))) @@ \
1.73 \ (Try (Repeat (Rewrite square_equation_left True))) @@ \
1.74 \ (Try (Repeat (Rewrite radd_0 False)))))\
1.75 - \ e_ ");
1.76 + \ e_e ");
1.77 atomty sc;
1.78 val (dI',pI',mI') = ("Test.thy",["sqroot-test","univariate","equation","test"],
1.79 ["Test","sqrt-equ-test"]);