1.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Wed Sep 08 16:45:27 2010 +0200
1.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Wed Sep 08 16:47:22 2010 +0200
1.3 @@ -129,7 +129,7 @@
1.4 (* --vvv-- ausgeliehen von test-root-equ/sml *)
1.5 val loc = e_istate;
1.6 val (dI',pI',mI') =
1.7 - ("Script.thy",["sqroot-test","univariate","equation"],
1.8 + ("Script",["sqroot-test","univariate","equation"],
1.9 ["Script","squ-equ-test2"]);
1.10 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
1.11 "solveFor x","errorBound (eps=0)",
1.12 @@ -266,7 +266,7 @@
1.13 "interval {x::real. 0 <= x & x <= pi}",
1.14 "errorBound (eps=(0::real))"];
1.15 val (dI',pI',mI') =
1.16 - ("DiffApp.thy",["maximum_of","function"],
1.17 + ("DiffApp",["maximum_of","function"],
1.18 ["DiffApp","max_by_calculus"]);
1.19
1.20 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.21 @@ -295,7 +295,7 @@
1.22 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.23
1.24 (*since 0508 Apply_Method does the 1st step, if NONE init_form -------------
1.25 -(*val nxt = ("Subproblem",Subproblem ("DiffApp.thy",["make","function"]))*)
1.26 +(*val nxt = ("Subproblem",Subproblem ("DiffApp",["make","function"]))*)
1.27 val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn_G e;
1.28 (*val nxt = ("Refine_Tacitly",Refine_Tacitly ["make","function"])*)
1.29 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.30 @@ -339,7 +339,7 @@
1.31 # presumerably didnt work before either, but not detected due to Emtpy_Tac #
1.32 ############################################################################
1.33
1.34 -(*val nxt = Subproblem ("DiffApp.thy",["univariate","equation"])) *)
1.35 +(*val nxt = Subproblem ("DiffApp",["univariate","equation"])) *)
1.36 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.37 (*val nxt = Refine_Tacitly ["univariate","equation"])*)
1.38
1.39 @@ -407,7 +407,7 @@
1.40 "interval {x::real. 0 <= x & x <= pi}",
1.41 "errorBound (eps=(0::real))"];
1.42 val (dI',pI',mI') =
1.43 - ("DiffApp.thy",["maximum_of","function"],
1.44 + ("DiffApp",["maximum_of","function"],
1.45 ["DiffApp","max_by_calculus"]);
1.46
1.47 CalcTree [(fmz, (dI',pI',mI'))];
1.48 @@ -444,7 +444,7 @@
1.49 "--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------";
1.50 str2term
1.51 "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\
1.52 - \ (v_::real) (itv_::real set) (err_::bool) = \
1.53 + \ (v_v::real) (itv_v::real set) (err_::bool) = \
1.54 \ (let e_e = (hd o (filterVar m_)) rs_; \
1.55 \ t_ = (if 1 < length_ rs_ \
1.56 \ then (SubProblem (Reals_,[make,function],[no_met])\
1.57 @@ -463,9 +463,9 @@
1.58 str2term "A");
1.59 val rs_ = (str2term "rs_::bool list",
1.60 str2term "[A = a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]");
1.61 -val v_v = (str2term "v_::real",
1.62 +val v_v = (str2term "v_v::real",
1.63 str2term "b");
1.64 -val itv_ = (str2term "itv_::real set",
1.65 +val itv_ = (str2term "itv_v::real set",
1.66 str2term "{x::real. 0 <= x & x <= 2*r}");
1.67 val err_ = (str2term "err_::bool",
1.68 str2term "eps=0");
1.69 @@ -519,7 +519,7 @@
1.70 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------";
1.71 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------";
1.72 str2term
1.73 - "Script Make_fun_by_explicit (f_::real) (v_::real) \
1.74 + "Script Make_fun_by_explicit (f_::real) (v_v::real) \
1.75 \ (eqs_::bool list) = \
1.76 \ (let h_ = (hd o (filterVar f_)) eqs_; \
1.77 \ e_1 = hd (dropWhile (ident h_) eqs_); \
1.78 @@ -530,7 +530,7 @@
1.79 \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)";
1.80 val f_ = (str2term "f_::real",
1.81 str2term "A");
1.82 -val v_v = (str2term "v_::real",
1.83 +val v_v = (str2term "v_v::real",
1.84 str2term "b");
1.85 val eqs_=(str2term "eqs_::bool list",
1.86 str2term "[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]");
1.87 @@ -610,7 +610,7 @@
1.88 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
1.89 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
1.90 str2term
1.91 - "Script Make_fun_by_new_variable (f_::real) (v_::real) \
1.92 + "Script Make_fun_by_new_variable (f_::real) (v_v::real) \
1.93 \ (eqs_::bool list) = \
1.94 \(let h_ = (hd o (filterVar f_)) eqs_; \
1.95 \ es_ = dropWhile (ident h_) eqs_; \
1.96 @@ -626,7 +626,7 @@
1.97 \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)";
1.98 val f_ = (str2term "f_::real",
1.99 str2term "A");
1.100 -val v_v = (str2term "v_::real",
1.101 +val v_v = (str2term "v_v::real",
1.102 str2term "alpha");
1.103 val eqs_=(str2term "eqs_::bool list",
1.104 str2term "[A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]");