1.1 --- a/src/Tools/isac/Knowledge/Diff.thy Wed Sep 08 16:45:27 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Wed Sep 08 16:47:22 2010 +0200
1.3 @@ -283,26 +283,26 @@
1.4 prls=e_rls, crls = Atools_erls, nrls = norm_diff},
1.5 "Script DiffScr (f_::real) (v_v::real) = " ^
1.6 " (let f'_ = Take (d_d v_v f_) " ^
1.7 -" in (((Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@ " ^
1.8 +" in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^
1.9 " (Repeat " ^
1.10 -" ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or " ^
1.11 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or " ^
1.12 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False)) Or " ^
1.13 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot True )) Or " ^
1.14 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False)) Or " ^
1.15 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False)) Or " ^
1.16 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False)) Or " ^
1.17 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False)) Or " ^
1.18 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False)) Or " ^
1.19 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False)) Or " ^
1.20 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False)) Or " ^
1.21 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or " ^
1.22 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or " ^
1.23 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or " ^
1.24 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or " ^
1.25 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or " ^
1.26 +" ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^
1.27 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^
1.28 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or " ^
1.29 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot True )) Or " ^
1.30 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or " ^
1.31 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or " ^
1.32 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or " ^
1.33 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or " ^
1.34 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or " ^
1.35 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or " ^
1.36 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or " ^
1.37 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or " ^
1.38 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^
1.39 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^
1.40 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^
1.41 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^
1.42 " (Repeat (Rewrite_Set make_polynomial False)))) @@ " ^
1.43 -" (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)))) f'_)"
1.44 +" (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f'_)"
1.45 ));
1.46
1.47 store_met
1.48 @@ -317,22 +317,22 @@
1.49 " (let f'_ = Take (d_d v_v f_) " ^
1.50 " in (( " ^
1.51 " (Repeat " ^
1.52 -" ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or " ^
1.53 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or " ^
1.54 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False)) Or " ^
1.55 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot True )) Or " ^
1.56 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False)) Or " ^
1.57 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False)) Or " ^
1.58 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False)) Or " ^
1.59 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False)) Or " ^
1.60 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False)) Or " ^
1.61 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False)) Or " ^
1.62 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False)) Or " ^
1.63 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or " ^
1.64 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or " ^
1.65 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or " ^
1.66 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or " ^
1.67 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or " ^
1.68 +" ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^
1.69 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^
1.70 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or " ^
1.71 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot True )) Or " ^
1.72 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or " ^
1.73 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or " ^
1.74 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or " ^
1.75 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or " ^
1.76 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or " ^
1.77 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or " ^
1.78 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or " ^
1.79 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or " ^
1.80 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^
1.81 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^
1.82 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^
1.83 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^
1.84 " (Repeat (Rewrite_Set make_polynomial False)))) " ^
1.85 " )) f'_)"
1.86 ));
1.87 @@ -347,27 +347,27 @@
1.88 srls = srls_diff, prls=e_rls, crls=Atools_erls, nrls = norm_diff},
1.89 "Script DiffEqScr (f_::bool) (v_v::real) = " ^
1.90 " (let f'_ = Take ((primed (lhs f_)) = d_d v_v (rhs f_)) " ^
1.91 -" in (((Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@ " ^
1.92 +" in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^
1.93 " (Repeat " ^
1.94 -" ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or " ^
1.95 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_dif False)) Or " ^
1.96 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or " ^
1.97 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False)) Or " ^
1.98 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot True )) Or " ^
1.99 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False)) Or " ^
1.100 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False)) Or " ^
1.101 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False)) Or " ^
1.102 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False)) Or " ^
1.103 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False)) Or " ^
1.104 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False)) Or " ^
1.105 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False)) Or " ^
1.106 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or " ^
1.107 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or " ^
1.108 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or " ^
1.109 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or " ^
1.110 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or " ^
1.111 +" ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^
1.112 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_dif False)) Or " ^
1.113 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^
1.114 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or " ^
1.115 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot True )) Or " ^
1.116 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or " ^
1.117 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or " ^
1.118 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or " ^
1.119 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or " ^
1.120 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or " ^
1.121 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or " ^
1.122 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or " ^
1.123 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or " ^
1.124 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^
1.125 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^
1.126 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^
1.127 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^
1.128 " (Repeat (Rewrite_Set make_polynomial False)))) @@ " ^
1.129 -" (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)))) f'_)"
1.130 +" (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f'_)"
1.131 ));
1.132
1.133 store_met
1.134 @@ -381,9 +381,9 @@
1.135 "Script DiffScr (f_::real) (v_v::real) = " ^
1.136 " (let f'_ = Take (d_d v_v f_) " ^
1.137 " in ((Try (Rewrite_Set norm_Rational False)) @@ " ^
1.138 -" (Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@ " ^
1.139 -" (Try (Rewrite_Set_Inst [(bdv,v_)] norm_diff False)) @@ " ^
1.140 -" (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)) @@ " ^
1.141 +" (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^
1.142 +" (Try (Rewrite_Set_Inst [(bdv,v_v)] norm_diff False)) @@ " ^
1.143 +" (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)) @@ " ^
1.144 " (Try (Rewrite_Set norm_Rational False))) f'_)"
1.145 ));
1.146
1.147 @@ -404,7 +404,7 @@
1.148 castab :=
1.149 overwritel (!castab,
1.150 [((term_of o the o (parse thy)) "Diff",
1.151 - (("Isac.thy", ["derivative_of","function"], ["no_met"]),
1.152 + (("Isac", ["derivative_of","function"], ["no_met"]),
1.153 argl2dtss))
1.154 ]);
1.155
1.156 @@ -422,7 +422,7 @@
1.157 castab :=
1.158 overwritel (!castab,
1.159 [((term_of o the o (parse thy)) "Differentiate",
1.160 - (("Isac.thy", ["named","derivative_of","function"], ["no_met"]),
1.161 + (("Isac", ["named","derivative_of","function"], ["no_met"]),
1.162 argl2dtss))
1.163 ]);
1.164 *}
2.1 --- a/src/Tools/isac/Knowledge/DiffApp-oldscr.sml Wed Sep 08 16:45:27 2010 +0200
2.2 +++ b/src/Tools/isac/Knowledge/DiffApp-oldscr.sml Wed Sep 08 16:47:22 2010 +0200
2.3 @@ -22,7 +22,7 @@
2.4 ML> set show_types;
2.5 ML> c;
2.6 val c =
2.7 - "Script1 Maximum_value fix_::bool list m_::real rs_::bool list v_v::real itv_::real set err_::bool =
2.8 + "Script1 Maximum_value fix_::bool list m_::real rs_::bool list v_v::real itv_v::real set err_::bool =
2.9 let e_e::bool = (hd o filter (Testvar m_)) rs_;
2.10 t_::real =
2.11 if (#1::real) < Length rs_
3.1 --- a/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml Wed Sep 08 16:45:27 2010 +0200
3.2 +++ b/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml Wed Sep 08 16:47:22 2010 +0200
3.3 @@ -315,7 +315,7 @@
3.4 "additionalRels [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
3.5 "additionalRels [A=#2*a*b - a^^^#2,a=#2*R*sin alpha, b=#2*R*cos alpha]"];
3.6 val (dI',pI',mI')=
3.7 - ("DiffAppl.thy",["Script.thy","maximum_of","function"],e_metID);
3.8 + ("DiffAppl",["Script","maximum_of","function"],e_metID);
3.9 val c = []:cid;
3.10
3.11 (*
3.12 @@ -416,7 +416,7 @@
3.13 "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
3.14 "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"];
3.15 val (dI',pI',mI')=
3.16 - ("DiffAppl.thy",["DiffAppl.thy","test_maximum"],e_metID);
3.17 + ("DiffAppl",["DiffAppl","test_maximum"],e_metID);
3.18 val p = e_pos'; val c = [];
3.19
3.20 val (mI,m) = ("Init_Proof",Init_Proof (cts, (dI',pI',mI')));
4.1 --- a/src/Tools/isac/Knowledge/DiffApp.sml Wed Sep 08 16:45:27 2010 +0200
4.2 +++ b/src/Tools/isac/Knowledge/DiffApp.sml Wed Sep 08 16:47:22 2010 +0200
4.3 @@ -3,17 +3,17 @@
4.4 *)
4.5
4.6
4.7 -theory' := overwritel (!theory', [("DiffAppl.thy",DiffAppl.thy)]);
4.8 +theory' := overwritel (!theory', [("DiffAppl",DiffAppl.thy)]);
4.9
4.10 (*
4.11 -> get_pbt ["DiffAppl.thy","maximum_of","function"];
4.12 -> get_met ("Script.thy","max_on_interval_by_calculus");
4.13 +> get_pbt ["DiffAppl","maximum_of","function"];
4.14 +> get_met ("Script","max_on_interval_by_calculus");
4.15 > !pbltypes;
4.16 *)
4.17 pbltypes:= overwritel (!pbltypes,
4.18 [
4.19 prep_pbt DiffAppl.thy
4.20 - (["DiffAppl.thy","maximum_of","function"],
4.21 + (["DiffAppl","maximum_of","function"],
4.22 [("#Given" ,"fixedValues fix_"),
4.23 ("#Find" ,"maximum m_"),
4.24 ("#Find" ,"valuesFor vs_"),
4.25 @@ -25,7 +25,7 @@
4.26 ]),
4.27
4.28 prep_pbt DiffAppl.thy
4.29 - (["DiffAppl.thy","make","function"]:pblID,
4.30 + (["DiffAppl","make","function"]:pblID,
4.31 [("#Given" ,"functionOf f_"),
4.32 ("#Given" ,"boundVariable v_v"),
4.33 ("#Given" ,"equalities eqs_"),
4.34 @@ -33,7 +33,7 @@
4.35 ]),
4.36
4.37 prep_pbt DiffAppl.thy
4.38 - (["DiffAppl.thy","on_interval","maximum_of","function"]:pblID,
4.39 + (["DiffAppl","on_interval","maximum_of","function"]:pblID,
4.40 [("#Given" ,"functionTerm t_"),
4.41 ("#Given" ,"boundVariable v_v"),
4.42 ("#Given" ,"interval itv_"),
4.43 @@ -41,7 +41,7 @@
4.44 ]),
4.45
4.46 prep_pbt DiffAppl.thy
4.47 - (["DiffAppl.thy","find_values","tool"]:pblID,
4.48 + (["DiffAppl","find_values","tool"]:pblID,
4.49 [("#Given" ,"maxArgument ma_"),
4.50 ("#Given" ,"functionTerm f_"),
4.51 ("#Given" ,"boundVariable v_v"),
4.52 @@ -53,7 +53,7 @@
4.53
4.54 methods:= overwritel (!methods,
4.55 [
4.56 - (("DiffAppl.thy","max_by_calculus"):metID,
4.57 + (("DiffAppl","max_by_calculus"):metID,
4.58 {ppc = prep_met DiffAppl.thy
4.59 [("#Given" ,"fixedValues fix_"),
4.60 ("#Given" ,"boundVariable v_v"),
4.61 @@ -66,7 +66,7 @@
4.62 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
4.63 scr=EmptyScr} : met),
4.64
4.65 - (("DiffAppl.thy","make_fun_by_new_variable"):metID,
4.66 + (("DiffAppl","make_fun_by_new_variable"):metID,
4.67 {ppc = prep_met DiffAppl.thy
4.68 [("#Given" ,"functionOf f_"),
4.69 ("#Given" ,"boundVariable v_v"),
4.70 @@ -76,7 +76,7 @@
4.71 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
4.72 scr=EmptyScr} : met),
4.73
4.74 - (("DiffAppl.thy","make_fun_by_explicit"):metID,
4.75 + (("DiffAppl","make_fun_by_explicit"):metID,
4.76 {ppc = prep_met DiffAppl.thy
4.77 [("#Given" ,"functionOf f_"),
4.78 ("#Given" ,"boundVariable v_v"),
4.79 @@ -86,7 +86,7 @@
4.80 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
4.81 scr=EmptyScr} : met),
4.82
4.83 - (("DiffAppl.thy","max_on_interval_by_calculus"):metID,
4.84 + (("DiffAppl","max_on_interval_by_calculus"):metID,
4.85 {ppc = prep_met DiffAppl.thy
4.86 [("#Given" ,"functionTerm t_"),
4.87 ("#Given" ,"boundVariable v_v"),
4.88 @@ -97,7 +97,7 @@
4.89 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
4.90 scr=EmptyScr} : met),
4.91
4.92 - (("DiffAppl.thy","find_values"):metID,
4.93 + (("DiffAppl","find_values"):metID,
4.94 {ppc = prep_met DiffAppl.thy
4.95 [],
4.96 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
5.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Wed Sep 08 16:45:27 2010 +0200
5.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Wed Sep 08 16:47:22 2010 +0200
5.3 @@ -162,7 +162,7 @@
5.4 crls = eval_rls, nrls=norm_Rational
5.5 (*, asm_rls=[],asm_thm=[]*)},
5.6 "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list) " ^
5.7 - " (v_v::real) (itv_::real set) (err_::bool) = " ^
5.8 + " (v_v::real) (itv_v::real set) (err_::bool) = " ^
5.9 " (let e_e = (hd o (filterVar m_)) rs_; " ^
5.10 " t_ = (if 1 < length_ rs_ " ^
5.11 " then (SubProblem (DiffApp_,[make,function],[no_met]) " ^
6.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed Sep 08 16:45:27 2010 +0200
6.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed Sep 08 16:47:22 2010 +0200
6.3 @@ -137,10 +137,10 @@
6.4 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
6.5 val _=writeln("t= f@ts= \""^
6.6 ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^
6.7 - (commas(map(string_of_cterm o cterm_of(sign_of thy)) ts))^"]\"");
6.8 + (commas(map(Syntax.string_of_term (thy2ctxt thy)) ts))^"]\"");
6.9 val _=writeln("u= g@us= \""^
6.10 ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^
6.11 - (commas(map(string_of_cterm o cterm_of(sign_of thy)) us))^"]\"");
6.12 + (commas(map(Syntax.string_of_term (thy2ctxt thy)) us))^"]\"");
6.13 val _=writeln("size_of_term(t,u)= ("^
6.14 (string_of_int(size_of_term' t))^", "^
6.15 (string_of_int(size_of_term' u))^")");
6.16 @@ -158,10 +158,10 @@
6.17 end
6.18 | ord => ord)
6.19 and hd_ord (f, g) = (* ~ term.ML *)
6.20 - prod_ord (prod_ord indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f,
6.21 + prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f,
6.22 dest_hd' g)
6.23 and terms_ord str pr (ts, us) =
6.24 - list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us);
6.25 + list_ord (term_ord' pr (assoc_thy "Isac"))(ts, us);
6.26 (**)
6.27 in
6.28 (**)
6.29 @@ -260,7 +260,7 @@
6.30 erls = Atools_erls, srls = Erls, calc = [],
6.31 rules = [Thm ("left_distrib",num_str @{thm left_distrib}),
6.32 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
6.33 - Thm ("nadd_divide_distrib",num_str @{thm nadd_divide_distrib}),
6.34 + Thm ("add_divide_distrib",num_str @{thm add_divide_distrib}),
6.35 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
6.36 (*^^^^^ *0* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
6.37 Rls_ norm_Rational_noadd_fractions(**2**),
7.1 --- a/src/Tools/isac/Knowledge/Equation.thy Wed Sep 08 16:45:27 2010 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Wed Sep 08 16:47:22 2010 +0200
7.3 @@ -78,10 +78,10 @@
7.4 castab :=
7.5 overwritel (!castab,
7.6 [((term_of o the o (parse thy)) "solveTest",
7.7 - (("Test.thy", ["univariate","equation","test"], ["no_met"]),
7.8 + (("Test", ["univariate","equation","test"], ["no_met"]),
7.9 argl2dtss)),
7.10 ((term_of o the o (parse thy)) "solve",
7.11 - (("Isac.thy", ["univariate","equation"], ["no_met"]),
7.12 + (("Isac", ["univariate","equation"], ["no_met"]),
7.13 argl2dtss))
7.14 ]);
7.15
8.1 --- a/src/Tools/isac/Knowledge/InsSort.sml Wed Sep 08 16:45:27 2010 +0200
8.2 +++ b/src/Tools/isac/Knowledge/InsSort.sml Wed Sep 08 16:47:22 2010 +0200
8.3 @@ -20,7 +20,7 @@
8.4
8.5 (*-------------------------from InsSort.ML 8.3.01----------------------*)
8.6
8.7 -theory' := (!theory') @ [("InsSort.thy",InsSort.thy)];
8.8 +theory' := (!theory') @ [("InsSort",InsSort.thy)];
8.9
8.10 val ins_sort =
8.11 Rls{preconds = [], rew_ord = ("tless_true",tless_true),
8.12 @@ -42,13 +42,13 @@
8.13
8.14
8.15 (*
8.16 -> get_pbt ["Script.thy","squareroot","univariate","equation"];
8.17 -> get_met ("Script.thy","max_on_interval_by_calculus");
8.18 +> get_pbt ["Script","squareroot","univariate","equation"];
8.19 +> get_met ("Script","max_on_interval_by_calculus");
8.20 *)
8.21 pbltypes:= (!pbltypes) @
8.22 [
8.23 prep_pbt InsSort.thy
8.24 - (["InsSort.thy","inssort"]:pblID,
8.25 + (["InsSort","inssort"]:pblID,
8.26 [("#Given" ,"unsorted u_"),
8.27 ("#Find" ,"sorted s_")
8.28 ])
8.29 @@ -57,13 +57,13 @@
8.30 methods:= (!methods) @
8.31 [
8.32 (*, -------17.6.00,
8.33 - (("InsSort.thy","inssort"):metID,
8.34 + (("InsSort","inssort"):metID,
8.35 {ppc = prep_met
8.36 [("#Given" ,"unsorted u_"),
8.37 ("#Find" ,"sorted s_")
8.38 ],
8.39 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
8.40 - scr=Script (((inst_abs (assoc_thm "InsSort.thy"))
8.41 + scr=Script (((inst_abs (assoc_thm "InsSort"))
8.42 o term_of o the o (parse thy)) (*for [#1,#3,#2] only*)
8.43 "Script Ins_sort (u_::'a list) = \
8.44 \ (let u_ = Rewrite sort_def False u_; \
8.45 @@ -85,7 +85,7 @@
8.46 \ in u_)")
8.47 } : met),
8.48
8.49 - (("InsSort.thy","sort"):metID,
8.50 + (("InsSort","sort"):metID,
8.51 {ppc = prep_met
8.52 [("#Given" ,"unsorted u_"),
8.53 ("#Find" ,"sorted s_")
9.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Wed Sep 08 16:45:27 2010 +0200
9.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Wed Sep 08 16:47:22 2010 +0200
9.3 @@ -241,8 +241,8 @@
9.4 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
9.5 Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})(*,
9.6 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
9.7 - *****Thm ("nadd_divide_distrib",
9.8 - *****num_str @{thm nadd_divide_distrib})
9.9 + *****Thm ("add_divide_distrib",
9.10 + *****num_str @{thm add_divide_distrib})
9.11 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)
9.12 ];
9.13 val simplify_Integral =
9.14 @@ -252,7 +252,7 @@
9.15 calc = [], (*asm_thm = [],*)
9.16 rules = [Thm ("left_distrib",num_str @{thm left_distrib}),
9.17 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
9.18 - Thm ("nadd_divide_distrib",num_str @{thm nadd_divide_distrib}),
9.19 + Thm ("add_divide_distrib",num_str @{thm add_divide_distrib}),
9.20 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
9.21 (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
9.22 Rls_ norm_Rational_noadd_fractions,
9.23 @@ -294,8 +294,8 @@
9.24 * (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
9.25 * Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})(*,
9.26 * (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
9.27 -* Thm ("nadd_divide_distrib",
9.28 -* num_str @{thm nadd_divide_distrib})
9.29 +* Thm ("add_divide_distrib",
9.30 +* num_str @{thm add_divide_distrib})
9.31 * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
9.32 * ]),
9.33 * Calc ("HOL.divide" ,eval_cancel "#divide_e")
9.34 @@ -369,7 +369,7 @@
9.35 crls = Atools_erls, nrls = e_rls},
9.36 "Script IntegrationScript (f_::real) (v_v::real) = " ^
9.37 " (let t_ = Take (Integral f_ D v_v) " ^
9.38 -" in (Rewrite_Set_Inst [(bdv,v_)] integration False) (t_::real))"
9.39 +" in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_::real))"
9.40 ));
9.41
9.42 store_met
9.43 @@ -384,8 +384,8 @@
9.44 crls = Atools_erls, nrls = e_rls},
9.45 "Script NamedIntegrationScript (f_::real) (v_v::real) (F_::real=>real) = " ^
9.46 " (let t_ = Take (F_ v_v = Integral f_ D v_v) " ^
9.47 -" in ((Try (Rewrite_Set_Inst [(bdv,v_)] simplify_Integral False)) @@ " ^
9.48 -" (Rewrite_Set_Inst [(bdv,v_)] integration False)) t_) "
9.49 +" in ((Try (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) @@ " ^
9.50 +" (Rewrite_Set_Inst [(bdv,v_v)] integration False)) t_) "
9.51 ));
9.52 *}
9.53
10.1 --- a/src/Tools/isac/Knowledge/LogExp.thy Wed Sep 08 16:45:27 2010 +0200
10.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy Wed Sep 08 16:47:22 2010 +0200
10.3 @@ -32,10 +32,10 @@
10.4 (prep_pbt thy "pbl_test_equ_univ_log" [] e_pblID
10.5 (["logarithmic","univariate","equation"],
10.6 [("#Given",["equality e_e","solveFor v_v"]),
10.7 - ("#Where",["matches ((?a log ?v_) = ?b) e_e"]),
10.8 + ("#Where",["matches ((?a log ?v_v) = ?b) e_e"]),
10.9 ("#Find" ,["solutions v_i"]),
10.10 - ("#With" ,["||(lhs (Subst (v_i_,v_) e_e) - " ^
10.11 - " (rhs (Subst (v_i_,v_) e_e) || < eps)"])
10.12 + ("#With" ,["||(lhs (Subst (v_i_,v_v) e_e) - " ^
10.13 + " (rhs (Subst (v_i_,v_v) e_e) || < eps)"])
10.14 ],
10.15 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
10.16 [["Equation","solve_log"]]));
10.17 @@ -45,7 +45,7 @@
10.18 (prep_met thy "met_equ_log" [] e_metID
10.19 (["Equation","solve_log"],
10.20 [("#Given" ,["equality e_e","solveFor v_v"]),
10.21 - ("#Where" ,["matches ((?a log ?v_) = ?b) e_e"]),
10.22 + ("#Where" ,["matches ((?a log ?v_v) = ?b) e_e"]),
10.23 ("#Find" ,["solutions v_i"])
10.24 ],
10.25 {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
11.1 --- a/src/Tools/isac/Knowledge/Poly.thy Wed Sep 08 16:45:27 2010 +0200
11.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Wed Sep 08 16:47:22 2010 +0200
11.3 @@ -475,7 +475,7 @@
11.4 and hd_ord (f, g) = (* ~ term.ML *)
11.5 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
11.6 and terms_ord str pr (ts, us) =
11.7 - list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us);
11.8 + list_ord (term_ord' pr (assoc_thy "Isac"))(ts, us);
11.9 in
11.10
11.11 fun ord_make_polynomial (pr:bool) thy (_:subst) tu =
12.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Wed Sep 08 16:45:27 2010 +0200
12.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Wed Sep 08 16:47:22 2010 +0200
12.3 @@ -1102,7 +1102,7 @@
12.4 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
12.5 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
12.6 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
12.7 - " in Check_elementwise L_L {(v_v::real). Assumptions} )"
12.8 + " in Check_elementwise L_LL {(v_v::real). Assumptions} )"
12.9 ));
12.10 *}
12.11 ML{*
12.12 @@ -1129,7 +1129,7 @@
12.13 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
12.14 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
12.15 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
12.16 - " in Check_elementwise L_L {(v_v::real). Assumptions} )"
12.17 + " in Check_elementwise L_LL {(v_v::real). Assumptions} )"
12.18 ));
12.19 *}
12.20 ML{*
12.21 @@ -1156,7 +1156,7 @@
12.22 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
12.23 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
12.24 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
12.25 - " in Check_elementwise L_L {(v_v::real). Assumptions} )"
12.26 + " in Check_elementwise L_LL {(v_v::real). Assumptions} )"
12.27 ));
12.28 *}
12.29 ML{*
12.30 @@ -1180,7 +1180,7 @@
12.31 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
12.32 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e; " ^
12.33 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
12.34 - " in Check_elementwise L_L {(v_v::real). Assumptions} )"
12.35 + " in Check_elementwise L_LL {(v_v::real). Assumptions} )"
12.36 ));
12.37 *}
12.38 ML{*
12.39 @@ -1204,7 +1204,7 @@
12.40 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
12.41 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
12.42 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
12.43 - " in Check_elementwise L_L {(v_v::real). Assumptions} )"
12.44 + " in Check_elementwise L_LL {(v_v::real). Assumptions} )"
12.45 ));
12.46 *}
12.47 ML{*
12.48 @@ -1228,7 +1228,7 @@
12.49 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
12.50 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
12.51 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
12.52 - " in Check_elementwise L_L {(v_v::real). Assumptions} )"
12.53 + " in Check_elementwise L_LL {(v_v::real). Assumptions} )"
12.54 ));
12.55 *}
12.56 ML{*
12.57 @@ -1258,7 +1258,7 @@
12.58 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
12.59 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
12.60 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
12.61 - " in Check_elementwise L_L {(v_v::real). Assumptions} )"
12.62 + " in Check_elementwise L_LL {(v_v::real). Assumptions} )"
12.63 ));
12.64 *}
12.65 ML{*
13.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Wed Sep 08 16:45:27 2010 +0200
13.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Wed Sep 08 16:47:22 2010 +0200
13.3 @@ -214,7 +214,7 @@
13.4 " (Repeat(Try (Rewrite_Set RatEq_eliminate True)))) e_e;" ^
13.5 " (L_L::bool list) = (SubProblem (RatEq',[univariate,equation], [no_met])" ^
13.6 " [BOOL e_e, REAL v_v]) " ^
13.7 - " in Check_elementwise L_L {(v_v::real). Assumptions})"
13.8 + " in Check_elementwise L_LL {(v_v::real). Assumptions})"
13.9 ));
13.10 *}
13.11
14.1 --- a/src/Tools/isac/Knowledge/Root.thy Wed Sep 08 16:45:27 2010 +0200
14.2 +++ b/src/Tools/isac/Knowledge/Root.thy Wed Sep 08 16:47:22 2010 +0200
14.3 @@ -140,7 +140,7 @@
14.4 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord
14.5 (dest_hd' f, dest_hd' g)
14.6 and terms_ord str pr (ts, us) =
14.7 - list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us);
14.8 + list_ord (term_ord' pr (assoc_thy "Isac"))(ts, us);
14.9
14.10 in
14.11 (* associates a+(b+c) => (a+b)+c = a+b+c ... avoiding parentheses
15.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Wed Sep 08 16:45:27 2010 +0200
15.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Wed Sep 08 16:47:22 2010 +0200
15.3 @@ -575,7 +575,7 @@
15.4 " [no_met]) [BOOL e_e, REAL v_v]) " ^
15.5 " else (SubProblem (RootEq',[univariate,equation], [no_met]) " ^
15.6 " [BOOL e_e, REAL v_v])) " ^
15.7 -"in Check_elementwise L_L {(v_v::real). Assumptions})"
15.8 +"in Check_elementwise L_LL {(v_v::real). Assumptions})"
15.9 ));
15.10 *}
15.11
16.1 --- a/src/Tools/isac/Knowledge/Test.sml Wed Sep 08 16:45:27 2010 +0200
16.2 +++ b/src/Tools/isac/Knowledge/Test.sml Wed Sep 08 16:47:22 2010 +0200
16.3 @@ -1,7 +1,7 @@
16.4 val ttt = (term_of o the o (parse thy))
16.5 -"(Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) e_e";
16.6 +"(Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) e_e";
16.7 val ttt = (term_of o the o (parse thy))
16.8 -"(Try (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) e_e)";
16.9 +"(Try (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) e_e)";
16.10
16.11 val ttt = (term_of o the o (parse thy))
16.12 "(Rewrite_Set SqRoot_simplify False) e_e ";
16.13 @@ -32,7 +32,7 @@
16.14 val ttt = (term_of o the o (parse thy))
16.15 "Script Solve_linear (e_e::bool) (v_v::real)= \
16.16 \(let e_e = \
16.17 - \ (Repeat ((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False)) e_e)\
16.18 + \ (Repeat ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False)) e_e)\
16.19 \ in [e_])";
16.20 (*----*)
16.21 val ttt = (term_of o the o (parse thy))
16.22 @@ -42,7 +42,7 @@
16.23 "Script Solve_linear (e_e::bool) (v_v::real)= \
16.24 \(let e_e = \
16.25 \ (Repeat\
16.26 - \ ((%ee_. (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) ee_)\
16.27 + \ ((%ee_. (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) ee_)\
16.28 \ e_e)\
16.29 \ e_e)\
16.30 \ in [e_])";
16.31 @@ -51,7 +51,7 @@
16.32 \(let e_e = \
16.33 \ (Repeat\
16.34 \ ((%ee_.\
16.35 - \ ((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) ee_))\
16.36 + \ ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) ee_))\
16.37 \ e_e)\
16.38 \ e_e)\
16.39 \ in [e_])";
16.40 @@ -60,7 +60,7 @@
16.41 \(let e_e = \
16.42 \ (Repeat\
16.43 \ ((%ee_.\
16.44 - \ (let e_e = ((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) ee_)\
16.45 + \ (let e_e = ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) ee_)\
16.46 \ in ((Rewrite_Set SqRoot_simplify False) e_e)) )\
16.47 \ e_e)\
16.48 \ e_e)\
16.49 @@ -121,22 +121,22 @@
16.50 "Script Solve_linear (e_e::bool) (v_v::real)= \
16.51 \(let e_e = \
16.52 \ ((Repeat\
16.53 - \ (((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\
16.54 + \ (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\
16.55 \ (Rewrite_Set SqRoot_simplify False)))) e_e)\
16.56 \ in [e_])";
16.57 atomty ttt;
16.58
16.59
16.60 val ttt = (term_of o the o (parse thy))
16.61 -"(Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@ yyy";
16.62 +"(Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@ yyy";
16.63 atomty ttt;
16.64 val ttt = (term_of o the o (parse thy))
16.65 - "(Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\
16.66 + "(Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\
16.67 \ (Rewrite_Set SqRoot_simplify False)";
16.68 atomty ttt;
16.69 val ttt = (term_of o the o (parse thy))
16.70 "(Repeat\
16.71 - \ ((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\
16.72 + \ ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\
16.73 \ (Rewrite_Set SqRoot_simplify False))) e_e";
16.74 atomty ttt;
16.75 val ttt = (term_of o the o (parseold thy))
16.76 @@ -150,7 +150,7 @@
16.77 "Script Solve_linear (e_e::bool) (v_v::real)= \
16.78 \(let e_e =\
16.79 \ Repeat\
16.80 - \ (((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\
16.81 + \ (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\
16.82 \ (Rewrite_Set SqRoot_simplify False))) e_\
16.83 \ in [e_::bool])"
16.84 ;
17.1 --- a/src/Tools/isac/Knowledge/Test.thy Wed Sep 08 16:45:27 2010 +0200
17.2 +++ b/src/Tools/isac/Knowledge/Test.thy Wed Sep 08 16:47:22 2010 +0200
17.3 @@ -597,7 +597,7 @@
17.4 "Script Solve_linear (e_e::bool) (v_v::real)= " ^
17.5 "(let e_e =" ^
17.6 " Repeat" ^
17.7 - " (((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@" ^
17.8 + " (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
17.9 " (Rewrite_Set Test_simplify False))) e_e" ^
17.10 " in [e_::bool])"
17.11 )
17.12 @@ -897,7 +897,7 @@
17.13 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
17.14 " (Try (Rewrite_Set norm_equation False)) @@" ^
17.15 " (Try (Rewrite_Set Test_simplify False)) @@" ^
17.16 - " (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@" ^
17.17 + " (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
17.18 " (Try (Rewrite_Set Test_simplify False)))" ^
17.19 " e_e" ^
17.20 " in [e_::bool])"
17.21 @@ -927,12 +927,12 @@
17.22 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
17.23 " (Try (Rewrite_Set norm_equation False)) @@" ^
17.24 " (Try (Rewrite_Set Test_simplify False)) @@" ^
17.25 - " (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@" ^
17.26 + " (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
17.27 " (Try (Rewrite_Set Test_simplify False)))" ^
17.28 - " e_;" ^
17.29 + " e_e;" ^
17.30 " (L_::bool list) = Tac subproblem_equation_dummy; " ^
17.31 - " L_ = Tac solve_equation_dummy " ^
17.32 - " in Check_elementwise L_ {(v_v::real). Assumptions})"
17.33 + " L_L = Tac solve_equation_dummy " ^
17.34 + " in Check_elementwise L_L {(v_v::real). Assumptions})"
17.35 ));
17.36
17.37 store_met
17.38 @@ -946,10 +946,10 @@
17.39 crls=tval_rls, nrls=Test_simplify},
17.40 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
17.41 " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@ " ^
17.42 - " (Try (Rewrite_Set Test_simplify False))) e_; " ^
17.43 + " (Try (Rewrite_Set Test_simplify False))) e_e; " ^
17.44 "(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^
17.45 " [Test,solve_linear]) [BOOL e_e, REAL v_])" ^
17.46 - "in Check_elementwise L_ {(v_v::real). Assumptions})"
17.47 + "in Check_elementwise L_L {(v_v::real). Assumptions})"
17.48 ));
17.49
17.50 store_met
17.51 @@ -964,10 +964,10 @@
17.52 asm_rls=[],asm_thm=[("square_equation_left",""),
17.53 ("square_equation_right","")]*)},
17.54 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
17.55 - " (let e_e = Try (Rewrite_Set norm_equation False) e_; " ^
17.56 + " (let e_e = Try (Rewrite_Set norm_equation False) e_e; " ^
17.57 "(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^
17.58 " [Test,solve_by_pq_formula]) [BOOL e_e, REAL v_])" ^
17.59 - "in Check_elementwise L_ {(v_v::real). Assumptions})"
17.60 + "in Check_elementwise L_L {(v_v::real). Assumptions})"
17.61 ));
17.62
17.63 store_met
17.64 @@ -994,11 +994,11 @@
17.65 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
17.66 " (Try (Rewrite_Set norm_equation False)) @@" ^
17.67 " (Try (Rewrite_Set Test_simplify False)))" ^
17.68 - " e_;" ^
17.69 + " e_e;" ^
17.70 " (L_::bool list) = " ^
17.71 " (SubProblem (Test_,[linear,univariate,equation,test]," ^
17.72 " [Test,solve_linear]) [BOOL e_e, REAL v_])" ^
17.73 - "in Check_elementwise L_ {(v_v::real). Assumptions})"
17.74 + "in Check_elementwise L_L {(v_v::real). Assumptions})"
17.75 ));
17.76
17.77 store_met
17.78 @@ -1025,10 +1025,10 @@
17.79 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
17.80 " (Try (Rewrite_Set norm_equation False)) @@" ^
17.81 " (Try (Rewrite_Set Test_simplify False)))" ^
17.82 - " e_;" ^
17.83 + " e_e;" ^
17.84 " (L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^
17.85 " [Test,solve_linear]) [BOOL e_e, REAL v_])" ^
17.86 - " in Check_elementwise L_ {(v_v::real). Assumptions})"
17.87 + " in Check_elementwise L_L {(v_v::real). Assumptions})"
17.88 ));
17.89
17.90 store_met
17.91 @@ -1056,10 +1056,10 @@
17.92 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
17.93 " (Try (Rewrite_Set norm_equation False)) @@" ^
17.94 " (Try (Rewrite_Set Test_simplify False)))" ^
17.95 - " e_;" ^
17.96 + " e_e;" ^
17.97 " (L_::bool list) = (SubProblem (Test_,[plain_square,univariate,equation,test]," ^
17.98 " [Test,solve_plain_square]) [BOOL e_e, REAL v_])" ^
17.99 - " in Check_elementwise L_ {(v_v::real). Assumptions})"
17.100 + " in Check_elementwise L_L {(v_v::real). Assumptions})"
17.101 ));
17.102
17.103 store_met
17.104 @@ -1087,10 +1087,10 @@
17.105 " (Try (Rewrite_Set Test_simplify False)))) @@" ^
17.106 " (Try (Rewrite_Set norm_equation False)) @@" ^
17.107 " (Try (Rewrite_Set Test_simplify False)))" ^
17.108 - " e_;" ^
17.109 + " e_e;" ^
17.110 " (L_::bool list) = (SubProblem (Test_,[univariate,equation,test]," ^
17.111 " [no_met]) [BOOL e_e, REAL v_])" ^
17.112 - " in Check_elementwise L_ {(v_v::real). Assumptions})"
17.113 + " in Check_elementwise L_L {(v_v::real). Assumptions})"
17.114 ) ); (*#######*)
17.115
17.116 store_met
17.117 @@ -1200,9 +1200,9 @@
17.118 end
17.119 | ord => ord)
17.120 and hd_ord (f, g) = (* ~ term.ML *)
17.121 - prod_ord (prod_ord indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
17.122 + prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
17.123 and terms_ord str pr (ts, us) =
17.124 - list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us);
17.125 + list_ord (term_ord' pr (assoc_thy "Isac"))(ts, us);
17.126 in
17.127
17.128 fun ord_make_polytest (pr:bool) thy (_:subst) tu =
18.1 --- a/test/Tools/isac/Knowledge/algein.sml Wed Sep 08 16:45:27 2010 +0200
18.2 +++ b/test/Tools/isac/Knowledge/algein.sml Wed Sep 08 16:47:22 2010 +0200
18.3 @@ -64,7 +64,7 @@
18.4 "KantenOben [t1 = k - 2*q, t2 = k - 2*q, t3 = k - 2*q, t4 = k - 2*q ]",
18.5 "GesamtLaenge L"];
18.6 val (dI',pI',mI') =
18.7 - ("Isac.thy",["numerischSymbolische", "Berechnung"],
18.8 + ("Isac",["numerischSymbolische", "Berechnung"],
18.9 ["Berechnung","erstNumerisch"]);
18.10 val p = e_pos'; val c = [];
18.11 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))](*nxt = ("Model_Pr*);
18.12 @@ -77,7 +77,7 @@
18.13 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenOben [b1 = k - 2 *q])*);
18.14 val (p,_,f,nxt,_,pt) = me nxt p c pt(*..KantenOben [b2 = k - 2 * q, b3 =, b4*);
18.15 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Find "GesamtLaenge L"*);
18.16 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Theory "AlgEin.thy"*);
18.17 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Theory "AlgEin"*);
18.18 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Problem ["numerischSymbolis,Be*);
18.19 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Method ["Berechnung", "erstSym*);
18.20 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Apply_Method*);
18.21 @@ -108,7 +108,7 @@
18.22 "KantenSenkrecht [v1 = k, v2 = k, v3 = k, v4 = k]",
18.23 "KantenOben [t1 = k - 2*q, t2 = k - 2*q, t3 = k - 2*q, t4 = k - 2*q ]",
18.24 "GesamtLaenge L"],
18.25 - ("Isac.thy",["numerischSymbolische", "Berechnung"],
18.26 + ("Isac",["numerischSymbolische", "Berechnung"],
18.27 ["Berechnung","erstSymbolisch"]))];
18.28 Iterator 1;
18.29 moveActiveRoot 1;
19.1 --- a/test/Tools/isac/Knowledge/biegelinie.sml Wed Sep 08 16:45:27 2010 +0200
19.2 +++ b/test/Tools/isac/Knowledge/biegelinie.sml Wed Sep 08 16:47:22 2010 +0200
19.3 @@ -54,7 +54,7 @@
19.4 "----------- Script [IntegrierenUndKonstanteBestimmen] -----------";
19.5 val str =
19.6 "Script BiegelinieScript \
19.7 -\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
19.8 +\(l_::real) (q__::real) (v_v::real) (b_::real=>real) \
19.9 \(rb_::bool list) (rm_::bool list) = \
19.10 \ (let q___ = Take (q_ v_v = q__); \
19.11 \ q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ \
19.12 @@ -181,7 +181,7 @@
19.13 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
19.14 "FunktionsVariable x"];
19.15 val (dI',pI',mI') =
19.16 - ("Biegelinie.thy",["MomentBestimmte","Biegelinien"],
19.17 + ("Biegelinie",["MomentBestimmte","Biegelinien"],
19.18 ["IntegrierenUndKonstanteBestimmen"]);
19.19 val p = e_pos'; val c = [];
19.20 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
19.21 @@ -213,7 +213,7 @@
19.22 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
19.23
19.24 case nxt of
19.25 - (_,Subproblem ("Biegelinie.thy", ["named", "integrate", "function"])) => ()
19.26 + (_,Subproblem ("Biegelinie", ["named", "integrate", "function"])) => ()
19.27 | _ => raise error "biegelinie.sml: Bsp 7.27 #4c";
19.28 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.29 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.30 @@ -231,7 +231,7 @@
19.31 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
19.32 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
19.33 case nxt of
19.34 - (_, Subproblem ("Biegelinie.thy", ["named", "integrate", "function"]))=>()
19.35 + (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
19.36 | _ => raise error "biegelinie.sml: Bsp 7.27 #5b";
19.37
19.38 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.39 @@ -259,7 +259,7 @@
19.40 if f2str f = "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2" then ()
19.41 else raise error "biegelinie.sml: Bsp 7.27 #9";
19.42
19.43 -(*val nxt = (+, Subproblem ("Biegelinie.thy", ["normalize", ..lin..sys]))*)
19.44 +(*val nxt = (+, Subproblem ("Biegelinie", ["normalize", ..lin..sys]))*)
19.45 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.46 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.47 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.48 @@ -299,7 +299,7 @@
19.49 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
19.50 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
19.51 case nxt of
19.52 - (_, Subproblem ("Biegelinie.thy", ["named", "integrate", "function"]))=>()
19.53 + (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
19.54 | _ => raise error "biegelinie.sml: Bsp 7.27 #13";
19.55
19.56 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.57 @@ -321,7 +321,7 @@
19.58 "y' x = c + 1 / (-1 * EI) * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
19.59 then () else raise error "biegelinie.sml: Bsp 7.27 #16 f";
19.60 case nxt of
19.61 - (_, Subproblem ("Biegelinie.thy", ["named", "integrate", "function"]))=>()
19.62 + (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
19.63 | _ => raise error "biegelinie.sml: Bsp 7.27 #16";
19.64
19.65 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.66 @@ -349,7 +349,7 @@
19.67 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
19.68 case nxt of
19.69 (_, Subproblem
19.70 - ("Biegelinie.thy", ["normalize", "2x2", "linear", "system"])) => ()
19.71 + ("Biegelinie", ["normalize", "2x2", "linear", "system"])) => ()
19.72 | _ => raise error "biegelinie.sml: Bsp 7.27 #19";
19.73 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.74 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.75 @@ -367,7 +367,7 @@
19.76 else raise error "biegelinie.sml: Bsp 7.27 #21 f";
19.77 case nxt of
19.78 (_, Subproblem
19.79 - ("Biegelinie.thy", ["triangular", "2x2", "linear", "system"])) =>()
19.80 + ("Biegelinie", ["triangular", "2x2", "linear", "system"])) =>()
19.81 | _ => raise error "biegelinie.sml: Bsp 7.27 #21";
19.82 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.83 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.84 @@ -454,7 +454,7 @@
19.85 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
19.86 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
19.87 "FunktionsVariable x"],
19.88 - ("Biegelinie.thy",
19.89 + ("Biegelinie",
19.90 ["MomentBestimmte","Biegelinien"],
19.91 ["IntegrierenUndKonstanteBestimmen"]))];
19.92 moveActiveRoot 1;
19.93 @@ -500,7 +500,7 @@
19.94 \M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\
19.95 \ y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\
19.96 \ y x = c_4 + c_3 * x + 1 / (-1 * EI) * (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)]"];
19.97 -val (dI',pI',mI') = ("Biegelinie.thy", ["vonBelastungZu","Biegelinien"],
19.98 +val (dI',pI',mI') = ("Biegelinie", ["vonBelastungZu","Biegelinien"],
19.99 ["Biegelinien","ausBelastung"]);
19.100 val p = e_pos'; val c = [];
19.101 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
19.102 @@ -618,7 +618,7 @@
19.103 val fmz = ["functionEq (M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)",
19.104 "substitution (M_b L = 0)",
19.105 "equality equ___"];
19.106 -val (dI',pI',mI') = ("Biegelinie.thy", ["makeFunctionTo","equation"],
19.107 +val (dI',pI',mI') = ("Biegelinie", ["makeFunctionTo","equation"],
19.108 ["Equation","fromFunction"]);
19.109 val p = e_pos'; val c = [];
19.110 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
19.111 @@ -764,7 +764,7 @@
19.112 \y x = c_4 + c_3 * x + 1 / (-1 * EI) * (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)]",
19.113 "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
19.114 "Gleichungen equs___"];
19.115 -val (dI',pI',mI') = ("Biegelinie.thy", ["setzeRandbedingungen","Biegelinien"],
19.116 +val (dI',pI',mI') = ("Biegelinie", ["setzeRandbedingungen","Biegelinien"],
19.117 ["Biegelinien","setzeRandbedingungenEin"]);
19.118 val p = e_pos'; val c = [];
19.119 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
19.120 @@ -920,7 +920,7 @@
19.121 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
19.122 "----- script ";
19.123 val str =
19.124 -"Script Belastung2BiegelScript (q__::real) (v_::real) = \
19.125 +"Script Belastung2BiegelScript (q__::real) (v_v::real) = \
19.126 \ (let q___ = Take (q_ v_v = q__); \
19.127 \ q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ \
19.128 \ (Rewrite Belastung_Querkraft True)) q___; \
19.129 @@ -954,7 +954,7 @@
19.130 val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
19.131 "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
19.132 "FunktionsVariable x"];
19.133 -val (dI',pI',mI') = ("Biegelinie.thy", ["Biegelinien"],
19.134 +val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
19.135 ["IntegrierenUndKonstanteBestimmen2"]);
19.136 val p = e_pos'; val c = [];
19.137 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
19.138 @@ -975,7 +975,7 @@
19.139
19.140 #b# prep_met ... (["Biegelinien","ausBelastung"],
19.141 ... ("#Given" ,["Streckenlast q__","FunktionsVariable v_v"]),
19.142 - "Script Belastung2BiegelScript (q__::real) (v_::real) = \
19.143 + "Script Belastung2BiegelScript (q__::real) (v_v::real) = \
19.144
19.145 #a#b# BOTH HAVE 2 ARGUMENTS q__ and v_v ...OK
19.146 ##########################################################################
19.147 @@ -989,7 +989,7 @@
19.148 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
19.149 "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = 0, y' 0 = 0]",
19.150 "FunktionsVariable x"],
19.151 - ("Biegelinie.thy", ["Biegelinien"],
19.152 + ("Biegelinie", ["Biegelinien"],
19.153 ["IntegrierenUndKonstanteBestimmen2"]))];
19.154 moveActiveRoot 1;
19.155 autoCalculate 1 CompleteCalc;
20.1 --- a/test/Tools/isac/Knowledge/diff.sml Wed Sep 08 16:45:27 2010 +0200
20.2 +++ b/test/Tools/isac/Knowledge/diff.sml Wed Sep 08 16:47:22 2010 +0200
20.3 @@ -86,7 +86,7 @@
20.4 "----------- for correction of diff_const ------------------------";
20.5 "----------- for correction of diff_const ------------------------";
20.6 (*re-evaluate this file, otherwise > *** ME_Isa: 'erls' not known*)
20.7 -val thy' = "Diff.thy";
20.8 +val thy' = "Diff";
20.9 val ct = "Not (x =!= a)";
20.10 rewrite_set thy' false "erls" ct;
20.11 val ct = "2 is_const";
20.12 @@ -127,7 +127,7 @@
20.13 " _________________ for correction of diff_quot _________________ ";
20.14 " _________________ for correction of diff_quot _________________ ";
20.15 " _________________ for correction of diff_quot _________________ ";
20.16 -val thy' = "Diff.thy";
20.17 +val thy' = "Diff";
20.18 val ct = "Not (x = 0)";
20.19 rewrite_set thy' false "erls" ct;
20.20
20.21 @@ -145,7 +145,7 @@
20.22 " _________________ differentiate by rewrite _________________ ";
20.23 " _________________ differentiate by rewrite _________________ ";
20.24 " _________________ differentiate by rewrite _________________ ";
20.25 -val thy' = "Diff.thy";
20.26 +val thy' = "Diff";
20.27 val ct = "d_d x (x ^^^ 2 + 3 * x + 4)";
20.28 "--- 1 ---";
20.29 val thm = ("diff_sum","");
20.30 @@ -197,7 +197,7 @@
20.31 val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)",
20.32 "differentiateFor x","derivative f_'_"];
20.33 val (dI',pI',mI') =
20.34 - ("Diff.thy",["derivative_of","function"],
20.35 + ("Diff",["derivative_of","function"],
20.36 ["diff","diff_simpl"]);
20.37 val p = e_pos'; val c = [];
20.38 "--- s1 ---";
20.39 @@ -258,7 +258,7 @@
20.40 trace_rewrite:=false;
20.41
20.42 val ct = "2 * x ^^^ (2 - 1) + 3 * 1 + 0";
20.43 - val SOME (ct',_) = rewrite_set "Isac.thy" false "make_polynomial" ct;
20.44 + val SOME (ct',_) = rewrite_set "Isac" false "make_polynomial" ct;
20.45
20.46 trace_rewrite:=true;
20.47 val t = str2term ct;
20.48 @@ -274,7 +274,7 @@
20.49 case string_of_thm thm of
20.50
20.51
20.52 - val Rewrite_Set' ("Diff.thy",false,"make_polynomial",ff,(ff',[])) = m;
20.53 + val Rewrite_Set' ("Diff",false,"make_polynomial",ff,(ff',[])) = m;
20.54 term2str ff; term2str ff';
20.55
20.56
20.57 @@ -285,7 +285,7 @@
20.58 val (p,_,f,nxt,_,pt) = me nxt p c pt;
20.59 "--- 8 ---";
20.60 (*val nxt =
20.61 -("Check_Postcond",Check_Postcond ("Diff.thy","differentiate_on_R"));*)
20.62 +("Check_Postcond",Check_Postcond ("Diff","differentiate_on_R"));*)
20.63 val (p,_,f,nxt,_,pt) = me nxt p c pt;
20.64 "--- 9 ---";
20.65 (*val nxt = ("End_Proof'",End_Proof');*)
20.66 @@ -303,35 +303,35 @@
20.67 " _________________ script-eval corrected _________________ ";
20.68 " _________________ script-eval corrected _________________ ";
20.69 " _________________ script-eval corrected _________________ ";
20.70 -val scr = Script (((inst_abs (assoc_thy "Test.thy")) o
20.71 +val scr = Script (((inst_abs (assoc_thy "Test")) o
20.72 term_of o the o (parse Diff.thy))
20.73 - "Script Differentiate (f_::real) (v_::real) = \
20.74 + "Script Differentiate (f_::real) (v_v::real) = \
20.75 \(let f_ = Try (Repeat (Rewrite frac_conv False f_)); \
20.76 \ f_ = Try (Repeat (Rewrite root_conv False f_)); \
20.77 \ f_ = Repeat \
20.78 - \ ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False f_)) Or \
20.79 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False f_)) Or \
20.80 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False f_)) Or \
20.81 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot False f_)) Or \
20.82 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False f_)) Or \
20.83 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False f_)) Or \
20.84 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False f_)) Or \
20.85 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False f_)) Or \
20.86 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False f_)) Or \
20.87 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False f_)) Or \
20.88 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False f_)) Or \
20.89 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False f_)) Or \
20.90 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False f_)) Or \
20.91 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False f_)) Or \
20.92 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False f_)) Or \
20.93 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False f_)) Or \
20.94 + \ ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False f_)) Or \
20.95 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False f_)) Or \
20.96 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False f_)) Or \
20.97 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot False f_)) Or \
20.98 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False f_)) Or \
20.99 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False f_)) Or \
20.100 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False f_)) Or \
20.101 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False f_)) Or \
20.102 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False f_)) Or \
20.103 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False f_)) Or \
20.104 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False f_)) Or \
20.105 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False f_)) Or \
20.106 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False f_)) Or \
20.107 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False f_)) Or \
20.108 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False f_)) Or \
20.109 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False f_)) Or \
20.110 \ (Repeat (Rewrite_Set Test_simplify False f_))); \
20.111 \ f_ = Try (Repeat (Rewrite sym_frac_conv False f_)) \
20.112 \ in Try (Repeat (Rewrite sym_root_conv False f_)))");
20.113 val d = e_rls;
20.114 val (dI',pI',mI') =
20.115 - ("Diff.thy",e_pblID,
20.116 - ("Diff.thy","differentiate_on_R"));
20.117 + ("Diff",e_pblID,
20.118 + ("Diff","differentiate_on_R"));
20.119 val p = e_pos'; val c = [];
20.120 val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));
20.121 val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree;
20.122 @@ -352,45 +352,45 @@
20.123 val (pt,_) = cappend_atomic pt[1]e_loc ct (Rewrite("test","")) ct Complete;
20.124 val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_sum","")));
20.125
20.126 -val NextStep(l1,m') = nxt_tac "Diff.thy" (pt,p) scr ets0 l0;
20.127 +val NextStep(l1,m') = nxt_tac "Diff" (pt,p) scr ets0 l0;
20.128 (*("diff_sum","")*)
20.129 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets1)] =
20.130 - locate_gen "Diff.thy" m' (pt,p) (scr,d) ets0 l0;
20.131 + locate_gen "Diff" m' (pt,p) (scr,d) ets0 l0;
20.132 val ets1 = (drop_last ets0) @ ets1;val pt = update_ets pt [] [(1,ets1)];
20.133 " --------------- 2. ---------------------------------------------";
20.134 val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_sum","")));
20.135 -val NextStep(l2,m') = nxt_tac "Diff.thy" (pt,p) scr ets1 l1;
20.136 +val NextStep(l2,m') = nxt_tac "Diff" (pt,p) scr ets1 l1;
20.137 (*("diff_sum","")*)
20.138 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
20.139 - locate_gen "Diff.thy" m' (pt,p) (scr,d) ets1 l1;
20.140 + locate_gen "Diff" m' (pt,p) (scr,d) ets1 l1;
20.141 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
20.142 " --------------- 3. ---------------------------------------------";
20.143 val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_prod_const","")));
20.144 -val NextStep(l3,m') = nxt_tac "Diff.thy" (pt,p) scr ets2 l2;
20.145 +val NextStep(l3,m') = nxt_tac "Diff" (pt,p) scr ets2 l2;
20.146 (*("diff_prod_const","")*)
20.147 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets3)] =
20.148 - locate_gen "Diff.thy" m' (pt,p) (scr,d) ets2 l2;
20.149 + locate_gen "Diff" m' (pt,p) (scr,d) ets2 l2;
20.150 val ets3 = (drop_last ets2) @ ets3; val pt = update_ets pt [] [(1,ets3)];
20.151 " --------------- 4. ---------------------------------------------";
20.152 val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_pow","")));
20.153 -val NextStep(l4,m') = nxt_tac "Diff.thy" (pt,p) scr ets3 l3;
20.154 +val NextStep(l4,m') = nxt_tac "Diff" (pt,p) scr ets3 l3;
20.155 (*("diff_pow","")*)
20.156 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets4)] =
20.157 - locate_gen "Diff.thy" m' (pt,p) (scr,d) ets3 l3;
20.158 + locate_gen "Diff" m' (pt,p) (scr,d) ets3 l3;
20.159 val ets4 = (drop_last ets3) @ ets4; val pt = update_ets pt [] [(1,ets4)];
20.160 " --------------- 5. ---------------------------------------------";
20.161 val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_const","")));
20.162 -val NextStep(l5,m') = nxt_tac "Diff.thy" (pt,p) scr ets4 l4;
20.163 +val NextStep(l5,m') = nxt_tac "Diff" (pt,p) scr ets4 l4;
20.164 (*("diff_const","")*)
20.165 val Steps[ (Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets5)] =
20.166 - locate_gen "Diff.thy" m' (pt,p) (scr,d) ets4 l4;
20.167 + locate_gen "Diff" m' (pt,p) (scr,d) ets4 l4;
20.168 val ets5 = (drop_last ets4) @ ets5; val pt = update_ets pt [] [(1,ets5)];
20.169 " --------------- 6. ---------------------------------------------";
20.170 val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_var","")));
20.171 -val NextStep(l6,m') = nxt_tac "Diff.thy" (pt,p) scr ets5 l5;
20.172 +val NextStep(l6,m') = nxt_tac "Diff" (pt,p) scr ets5 l5;
20.173 (*("diff_var","")ok; here was("diff_const","")because of wrong rule in *.thy*)
20.174 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets6)] =
20.175 - locate_gen "Diff.thy" m' (pt,p) (scr,d) ets5 l5;
20.176 + locate_gen "Diff" m' (pt,p) (scr,d) ets5 l5;
20.177 val ets6 = (drop_last ets5) @ ets6; val pt = update_ets pt [] [(1,ets6)];
20.178 " --------------- 7. ---------------------------------------------";
20.179 val Appl m'=applicable_in p pt (Rewrite_Set "Test_simplify");
20.180 @@ -412,7 +412,7 @@
20.181 val fmz = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))",
20.182 "differentiateFor x","derivative f_'_"];
20.183 val (dI',pI',mI') =
20.184 - ("Diff.thy",["derivative_of","function"],
20.185 + ("Diff",["derivative_of","function"],
20.186 ["diff","differentiate_on_R"]);
20.187 *)
20.188
20.189 @@ -427,7 +427,7 @@
20.190 val fmz = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))",
20.191 "differentiateFor x","derivative f_'_"];
20.192 val (dI',pI',mI') =
20.193 - ("Diff.thy",["derivative_of","function"],
20.194 + ("Diff",["derivative_of","function"],
20.195 ["diff","differentiate_on_R"]);
20.196 *)
20.197
20.198 @@ -439,7 +439,7 @@
20.199 val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)",
20.200 "differentiateFor x","derivative f_'_"];
20.201 val (dI',pI',mI') =
20.202 - ("Diff.thy",["derivative_of","function"],
20.203 + ("Diff",["derivative_of","function"],
20.204 ["diff","diff_simpl"]);
20.205 (*val p = e_pos'; val c = [];
20.206 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
20.207 @@ -452,7 +452,7 @@
20.208 val (p,_,f,nxt,_,pt) = me nxt p c pt;
20.209 val (p,_,f,nxt,_,pt) = me nxt p c pt;
20.210 val (p,_,f,nxt,_,pt) = me nxt p c pt;
20.211 -(*nxt = ("Apply_Method",Apply_Method ("Diff.thy","differentiate_on_R*)
20.212 +(*nxt = ("Apply_Method",Apply_Method ("Diff","differentiate_on_R*)
20.213 val (p,_,f,nxt,_,pt) = me nxt p c pt;
20.214
20.215 val (p,_,f,nxt,_,pt) = me nxt p c pt;
20.216 @@ -486,30 +486,30 @@
20.217 else raise error "diff.sml: diff.behav. in 'primed'";
20.218 atomty f'_;
20.219
20.220 -val str = "Script DiffEqScr (f_::bool) (v_::real) = \
20.221 +val str = "Script DiffEqScr (f_::bool) (v_v::real) = \
20.222 \ (let f'_ = Take ((primed (lhs f_)) = d_d v_v (rhs f_)) \
20.223 \ in (((Try (Repeat (Rewrite frac_conv False))) @@ \
20.224 \ (Try (Repeat (Rewrite root_conv False))) @@ \
20.225 \ (Try (Repeat (Rewrite realpow_pow False))) @@ \
20.226 \ (Repeat \
20.227 - \ ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or \
20.228 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or \
20.229 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False)) Or \
20.230 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot True )) Or \
20.231 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False)) Or \
20.232 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False)) Or \
20.233 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False)) Or \
20.234 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False)) Or \
20.235 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False)) Or \
20.236 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False)) Or \
20.237 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False)) Or \
20.238 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or \
20.239 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or \
20.240 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or \
20.241 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sqrt False)) Or \
20.242 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sqrt_chain False)) Or \
20.243 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or \
20.244 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or \
20.245 + \ ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or \
20.246 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or \
20.247 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or \
20.248 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot True )) Or \
20.249 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or \
20.250 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or \
20.251 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or \
20.252 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or \
20.253 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or \
20.254 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or \
20.255 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or \
20.256 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or \
20.257 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or \
20.258 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or \
20.259 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sqrt False)) Or \
20.260 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sqrt_chain False)) Or \
20.261 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or \
20.262 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or \
20.263 \ (Repeat (Rewrite_Set make_polynomial False)))) @@ \
20.264 \ (Try (Repeat (Rewrite sym_frac_conv False))) @@ \
20.265 \ (Try (Repeat (Rewrite sym_root_conv False))))) f'_)"
20.266 @@ -568,7 +568,7 @@
20.267 [(["functionTerm (x^2 + x+ 1/x + 2/x^2)",
20.268 (*"functionTerm ((x^3)^5)",*)
20.269 "differentiateFor x", "derivative f_'_"],
20.270 - ("Isac.thy", ["derivative_of","function"],
20.271 + ("Isac", ["derivative_of","function"],
20.272 ["diff","differentiate_on_R"]))];
20.273 Iterator 1;
20.274 moveActiveRoot 1;
20.275 @@ -583,7 +583,7 @@
20.276 CalcTree
20.277 [(["functionTerm (x^3 * x^5)",
20.278 "differentiateFor x", "derivative f_'_"],
20.279 - ("Isac.thy", ["derivative_of","function"],
20.280 + ("Isac", ["derivative_of","function"],
20.281 ["diff","differentiate_on_R"]))];
20.282 Iterator 1;
20.283 moveActiveRoot 1;
20.284 @@ -608,7 +608,7 @@
20.285 CalcTree
20.286 [(["functionTerm (x^3 * x^5)",
20.287 "differentiateFor x", "derivative f_'_"],
20.288 - ("Isac.thy", ["derivative_of","function"],
20.289 + ("Isac", ["derivative_of","function"],
20.290 ["diff","after_simplification"]))];
20.291 Iterator 1;
20.292 moveActiveRoot 1;
20.293 @@ -628,7 +628,7 @@
20.294 CalcTree
20.295 [(["functionTerm ((x^3)^5)",
20.296 "differentiateFor x", "derivative f_'_"],
20.297 - ("Isac.thy", ["derivative_of","function"],
20.298 + ("Isac", ["derivative_of","function"],
20.299 ["diff","after_simplification"]))];
20.300 Iterator 1;
20.301 moveActiveRoot 1;
20.302 @@ -645,7 +645,7 @@
20.303 states:=[];
20.304 CalcTree
20.305 [(["functionEq (A = s * (a - s))", "differentiateFor s", "derivativeEq f_'_"],
20.306 - ("Isac.thy", ["named","derivative_of","function"],
20.307 + ("Isac", ["named","derivative_of","function"],
20.308 ["diff","differentiate_equality"]))];
20.309 Iterator 1;
20.310 moveActiveRoot 1;
20.311 @@ -677,7 +677,7 @@
20.312 CalcTree
20.313 [(["functionTerm (x^2 + x + 1)",
20.314 "differentiateFor x", "derivative f_'_"],
20.315 - ("Isac.thy", ["derivative_of","function"],
20.316 + ("Isac", ["derivative_of","function"],
20.317 ["diff","differentiate_on_R"]))];
20.318 Iterator 1;
20.319 moveActiveRoot 1;
21.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Wed Sep 08 16:45:27 2010 +0200
21.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Wed Sep 08 16:47:22 2010 +0200
21.3 @@ -129,7 +129,7 @@
21.4 (* --vvv-- ausgeliehen von test-root-equ/sml *)
21.5 val loc = e_istate;
21.6 val (dI',pI',mI') =
21.7 - ("Script.thy",["sqroot-test","univariate","equation"],
21.8 + ("Script",["sqroot-test","univariate","equation"],
21.9 ["Script","squ-equ-test2"]);
21.10 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
21.11 "solveFor x","errorBound (eps=0)",
21.12 @@ -266,7 +266,7 @@
21.13 "interval {x::real. 0 <= x & x <= pi}",
21.14 "errorBound (eps=(0::real))"];
21.15 val (dI',pI',mI') =
21.16 - ("DiffApp.thy",["maximum_of","function"],
21.17 + ("DiffApp",["maximum_of","function"],
21.18 ["DiffApp","max_by_calculus"]);
21.19
21.20 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
21.21 @@ -295,7 +295,7 @@
21.22 val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.23
21.24 (*since 0508 Apply_Method does the 1st step, if NONE init_form -------------
21.25 -(*val nxt = ("Subproblem",Subproblem ("DiffApp.thy",["make","function"]))*)
21.26 +(*val nxt = ("Subproblem",Subproblem ("DiffApp",["make","function"]))*)
21.27 val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn_G e;
21.28 (*val nxt = ("Refine_Tacitly",Refine_Tacitly ["make","function"])*)
21.29 val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.30 @@ -339,7 +339,7 @@
21.31 # presumerably didnt work before either, but not detected due to Emtpy_Tac #
21.32 ############################################################################
21.33
21.34 -(*val nxt = Subproblem ("DiffApp.thy",["univariate","equation"])) *)
21.35 +(*val nxt = Subproblem ("DiffApp",["univariate","equation"])) *)
21.36 val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.37 (*val nxt = Refine_Tacitly ["univariate","equation"])*)
21.38
21.39 @@ -407,7 +407,7 @@
21.40 "interval {x::real. 0 <= x & x <= pi}",
21.41 "errorBound (eps=(0::real))"];
21.42 val (dI',pI',mI') =
21.43 - ("DiffApp.thy",["maximum_of","function"],
21.44 + ("DiffApp",["maximum_of","function"],
21.45 ["DiffApp","max_by_calculus"]);
21.46
21.47 CalcTree [(fmz, (dI',pI',mI'))];
21.48 @@ -444,7 +444,7 @@
21.49 "--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------";
21.50 str2term
21.51 "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\
21.52 - \ (v_::real) (itv_::real set) (err_::bool) = \
21.53 + \ (v_v::real) (itv_v::real set) (err_::bool) = \
21.54 \ (let e_e = (hd o (filterVar m_)) rs_; \
21.55 \ t_ = (if 1 < length_ rs_ \
21.56 \ then (SubProblem (Reals_,[make,function],[no_met])\
21.57 @@ -463,9 +463,9 @@
21.58 str2term "A");
21.59 val rs_ = (str2term "rs_::bool list",
21.60 str2term "[A = a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]");
21.61 -val v_v = (str2term "v_::real",
21.62 +val v_v = (str2term "v_v::real",
21.63 str2term "b");
21.64 -val itv_ = (str2term "itv_::real set",
21.65 +val itv_ = (str2term "itv_v::real set",
21.66 str2term "{x::real. 0 <= x & x <= 2*r}");
21.67 val err_ = (str2term "err_::bool",
21.68 str2term "eps=0");
21.69 @@ -519,7 +519,7 @@
21.70 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------";
21.71 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------";
21.72 str2term
21.73 - "Script Make_fun_by_explicit (f_::real) (v_::real) \
21.74 + "Script Make_fun_by_explicit (f_::real) (v_v::real) \
21.75 \ (eqs_::bool list) = \
21.76 \ (let h_ = (hd o (filterVar f_)) eqs_; \
21.77 \ e_1 = hd (dropWhile (ident h_) eqs_); \
21.78 @@ -530,7 +530,7 @@
21.79 \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)";
21.80 val f_ = (str2term "f_::real",
21.81 str2term "A");
21.82 -val v_v = (str2term "v_::real",
21.83 +val v_v = (str2term "v_v::real",
21.84 str2term "b");
21.85 val eqs_=(str2term "eqs_::bool list",
21.86 str2term "[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]");
21.87 @@ -610,7 +610,7 @@
21.88 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
21.89 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
21.90 str2term
21.91 - "Script Make_fun_by_new_variable (f_::real) (v_::real) \
21.92 + "Script Make_fun_by_new_variable (f_::real) (v_v::real) \
21.93 \ (eqs_::bool list) = \
21.94 \(let h_ = (hd o (filterVar f_)) eqs_; \
21.95 \ es_ = dropWhile (ident h_) eqs_; \
21.96 @@ -626,7 +626,7 @@
21.97 \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)";
21.98 val f_ = (str2term "f_::real",
21.99 str2term "A");
21.100 -val v_v = (str2term "v_::real",
21.101 +val v_v = (str2term "v_v::real",
21.102 str2term "alpha");
21.103 val eqs_=(str2term "eqs_::bool list",
21.104 str2term "[A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]");
22.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Wed Sep 08 16:45:27 2010 +0200
22.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Wed Sep 08 16:47:22 2010 +0200
22.3 @@ -865,7 +865,7 @@
22.4 \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]",
22.5 "solveForVars [c, c_2]", "solution L"];
22.6 val (dI',pI',mI') =
22.7 - ("Biegelinie.thy",["normalize", "2x2", "linear", "system"],
22.8 + ("Biegelinie",["normalize", "2x2", "linear", "system"],
22.9 ["EqSystem","normalize","2x2"]);
22.10 val p = e_pos'; val c = [];
22.11 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
22.12 @@ -883,7 +883,7 @@
22.13 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
22.14 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
22.15 case nxt of
22.16 - (_, Subproblem ("Biegelinie.thy", ["triangular", "2x2", "linear",_])) => ()
22.17 + (_, Subproblem ("Biegelinie", ["triangular", "2x2", "linear",_])) => ()
22.18 | _ => raise error "eqsystem.sml me [EqSystem,normalize,2x2] SubProblem";
22.19
22.20 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
22.21 @@ -933,7 +933,7 @@
22.22 \ -1 * q_0 / 24 * L ^^^ 4)]",
22.23 "solveForVars [c, c_2]", "solution L"];
22.24 val (dI',pI',mI') =
22.25 - ("Biegelinie.thy",["linear", "system"], ["no_met"]);
22.26 + ("Biegelinie",["linear", "system"], ["no_met"]);
22.27 val p = e_pos'; val c = [];
22.28 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
22.29 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
22.30 @@ -952,7 +952,7 @@
22.31 "[c_2 = 0, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]"
22.32 then () else raise error "eqsystem.sml me simpl. before SubProblem b";
22.33 case nxt of
22.34 - (_, Subproblem ("Biegelinie.thy", ["triangular", "2x2", "linear",_])) => ()
22.35 + (_, Subproblem ("Biegelinie", ["triangular", "2x2", "linear",_])) => ()
22.36 | _ => raise error "eqsystem.sml me [linear,system] SubProblem b";
22.37
22.38 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
22.39 @@ -1004,7 +1004,7 @@
22.40 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
22.41 "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
22.42 "FunktionsVariable x"],
22.43 - ("Biegelinie.thy", ["Biegelinien"],
22.44 + ("Biegelinie", ["Biegelinien"],
22.45 ["IntegrierenUndKonstanteBestimmen2"]))];
22.46 moveActiveRoot 1;
22.47 (*
22.48 @@ -1045,7 +1045,7 @@
22.49 "Biegelinie y",
22.50 "Randbedingungen [y L = 0, y' L = 0]",
22.51 "FunktionsVariable x"],
22.52 - ("Biegelinie.thy", ["vonMomentenlinieZu","Biegelinien"],
22.53 + ("Biegelinie", ["vonMomentenlinieZu","Biegelinien"],
22.54 ["Biegelinien", "AusMomentenlinie"]))];
22.55 moveActiveRoot 1;
22.56 (*
22.57 @@ -1057,7 +1057,7 @@
22.58 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
22.59 "Randbedingungen [y 0 = 0, y L = 0, y' 0 = 0, y' L = 0]",
22.60 "FunktionsVariable x"],
22.61 - ("Biegelinie.thy", ["Biegelinien"],
22.62 + ("Biegelinie", ["Biegelinien"],
22.63 ["IntegrierenUndKonstanteBestimmen2"] ))];
22.64 moveActiveRoot 1;
22.65 (*
22.66 @@ -1077,7 +1077,7 @@
22.67 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
22.68 "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = 0, y' 0 = 0]",
22.69 "FunktionsVariable x"],
22.70 - ("Biegelinie.thy", ["Biegelinien"],
22.71 + ("Biegelinie", ["Biegelinien"],
22.72 ["IntegrierenUndKonstanteBestimmen2"] ))];
22.73 moveActiveRoot 1;
22.74 (*
22.75 @@ -1125,7 +1125,7 @@
22.76 \ 0 = c_3]",
22.77 "solveForVars [c, c_2, c_3, c_4]", "solution L"];
22.78 val (dI',pI',mI') =
22.79 - ("Biegelinie.thy",["linear", "system"],["no_met"]);
22.80 + ("Biegelinie",["linear", "system"],["no_met"]);
22.81 val p = e_pos'; val c = [];
22.82 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
22.83 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
22.84 @@ -1303,7 +1303,7 @@
22.85 \[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]",
22.86 "solveForVars [c, c_2, c_3, c_4]", "solution L"];
22.87 val (dI',pI',mI') =
22.88 - ("Biegelinie.thy",["linear", "system"],["no_met"]);
22.89 + ("Biegelinie",["linear", "system"],["no_met"]);
22.90 val p = e_pos'; val c = [];
22.91 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
22.92 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
22.93 @@ -1328,7 +1328,7 @@
22.94 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
22.95 "Randbedingungen [M_b L = 0, y 0 = 0, y L = 0, y' 0 = 0]",
22.96 "FunktionsVariable x"],
22.97 - ("Biegelinie.thy", ["Biegelinien"],
22.98 + ("Biegelinie", ["Biegelinien"],
22.99 ["IntegrierenUndKonstanteBestimmen2"] ))];
22.100 moveActiveRoot 1;
22.101 (*
22.102 @@ -1350,7 +1350,7 @@
22.103 "Biegelinie y",
22.104 "Randbedingungen [y 0 = 0, y L = 0]",
22.105 "FunktionsVariable x"],
22.106 - ("Biegelinie.thy", ["vonMomentenlinieZu","Biegelinien"],
22.107 + ("Biegelinie", ["vonMomentenlinieZu","Biegelinien"],
22.108 ["Biegelinien", "AusMomentenlinie"]))];
22.109 moveActiveRoot 1;
22.110 (*
22.111 @@ -1362,7 +1362,7 @@
22.112 CalcTree [(["Traegerlaenge L","Streckenlast (q_0 / L * x)","Biegelinie y",
22.113 "Randbedingungen [M_b 0 = 0, M_b L = 0, y 0 = 0, y L = 0]",
22.114 "FunktionsVariable x"],
22.115 - ("Biegelinie.thy", ["Biegelinien"],
22.116 + ("Biegelinie", ["Biegelinien"],
22.117 ["IntegrierenUndKonstanteBestimmen2"] ))];
22.118 moveActiveRoot 1;
22.119 (*
22.120 @@ -1383,7 +1383,7 @@
22.121 "Biegelinie y",
22.122 "Randbedingungen [y L = 0, y' L = 0]",
22.123 "FunktionsVariable x"],
22.124 - ("Biegelinie.thy", ["vonMomentenlinieZu","Biegelinien"],
22.125 + ("Biegelinie", ["vonMomentenlinieZu","Biegelinien"],
22.126 ["Biegelinien", "AusMomentenlinie"]))];
22.127 moveActiveRoot 1;
22.128 (*
22.129 @@ -1403,7 +1403,7 @@
22.130 \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]",
22.131 "solveForVars [c, c_2, c_3, c_4]", "solution L"];
22.132 val (dI',pI',mI') =
22.133 - ("Biegelinie.thy",["normalize", "4x4", "linear", "system"],
22.134 + ("Biegelinie",["normalize", "4x4", "linear", "system"],
22.135 ["EqSystem","normalize","4x4"]);
22.136 val p = e_pos'; val c = [];
22.137 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
23.1 --- a/test/Tools/isac/Knowledge/inssort.sml Wed Sep 08 16:45:27 2010 +0200
23.2 +++ b/test/Tools/isac/Knowledge/inssort.sml Wed Sep 08 16:47:22 2010 +0200
23.3 @@ -6,7 +6,7 @@
23.4 WN.7.6.03: -"- started with someList :: 'a list => unl, fun dest_list *)
23.5
23.6 "--------------- sort [1,4,3,2] by rewrite_set ----------------";
23.7 -val thy' = "InsSort.thy";
23.8 +val thy' = "InsSort";
23.9 val ct = "sort [1,4,3,2]";
23.10 "--- 1 ---";
23.11 val rls = "ins_sort";
23.12 @@ -16,7 +16,7 @@
23.13
23.14
23.15 "---------------- sort [1,3,2] by rewrite stepwise ----------------";
23.16 -val thy' = "InsSort.thy";
23.17 +val thy' = "InsSort";
23.18 val ct = "sort [1,3,2]";
23.19 "--- 1 ---";
23.20 val thm = ("sort_def","");
23.21 @@ -89,7 +89,7 @@
23.22 "---------------- sort [1,3,2] from script ----------------";
23.23 val fmz = ["unsorted [1,3,2]", "sorted S"];
23.24 val (dI',pI',mI') =
23.25 - ("InsSort.thy", ["inssort","functional"], ("InsSort.thy","inssort"));
23.26 + ("InsSort", ["inssort","functional"], ("InsSort","inssort"));
23.27 val p = e_pos'; val c = [];
23.28
23.29
24.1 --- a/test/Tools/isac/Knowledge/integrate.sml Wed Sep 08 16:45:27 2010 +0200
24.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Wed Sep 08 16:47:22 2010 +0200
24.3 @@ -248,7 +248,7 @@
24.4 val rls = "integration_rules";
24.5 val subs = [("bdv","x::real")];
24.6 fun rewrit_sinst subs rls str =
24.7 - fst (the (rewrite_set_inst "Integrate.thy" true subs rls str));
24.8 + fst (the (rewrite_set_inst "Integrate" true subs rls str));
24.9 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
24.10 val str = rewrit_sinst subs rls "Integral x D x";
24.11 val str = rewrit_sinst subs rls "Integral c * x ^^^ 2 + c_2 D x";
24.12 @@ -362,16 +362,16 @@
24.13 "----------- check Scripts ---------------------------------------";
24.14 "----------- check Scripts ---------------------------------------";
24.15 val str =
24.16 -"Script IntegrationScript (f_::real) (v_::real) = \
24.17 +"Script IntegrationScript (f_::real) (v_v::real) = \
24.18 \ (let t_ = Take (Integral f_ D v_v) \
24.19 -\ in (Rewrite_Set_Inst [(bdv,v_)] integration False) (t_::real))";
24.20 +\ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_::real))";
24.21 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
24.22 atomty sc;
24.23
24.24 val str =
24.25 -"Script NamedIntegrationScript (f_::real) (v_::real) (F_::real=>real) = \
24.26 +"Script NamedIntegrationScript (f_::real) (v_v::real) (F_::real=>real) = \
24.27 \ (let t_ = Take (F_ v_v = Integral f_ D v_v) \
24.28 -\ in (Rewrite_Set_Inst [(bdv,v_)] integration False) t_)";
24.29 +\ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) t_)";
24.30 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
24.31 atomty sc;
24.32 show_mets();
24.33 @@ -384,7 +384,7 @@
24.34 val fmz = ["functionTerm (x^^^2 + 1)",
24.35 "integrateBy x","antiDerivative FF"];
24.36 val (dI',pI',mI') =
24.37 - ("Integrate.thy",["integrate","function"],
24.38 + ("Integrate",["integrate","function"],
24.39 ["diff","integration"]);
24.40 val p = e_pos'; val c = [];
24.41 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
24.42 @@ -409,7 +409,7 @@
24.43 val fmz = ["functionTerm (x^^^2 + 1)",
24.44 "integrateBy x","antiDerivativeName F"];
24.45 val (dI',pI',mI') =
24.46 - ("Integrate.thy",["named","integrate","function"],
24.47 + ("Integrate",["named","integrate","function"],
24.48 ["diff","integration","named"]);
24.49 val p = e_pos'; val c = [];
24.50 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
24.51 @@ -434,7 +434,7 @@
24.52 val fmz = ["functionTerm (- q_0)",
24.53 "integrateBy x","antiDerivativeName Q"];
24.54 val (dI',pI',mI') =
24.55 - ("Biegelinie.thy",["named","integrate","function"],
24.56 + ("Biegelinie",["named","integrate","function"],
24.57 ["diff","integration","named"]);
24.58 val p = e_pos'; val c = [];
24.59 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
24.60 @@ -460,7 +460,7 @@
24.61 states:=[];
24.62 CalcTree
24.63 [(["functionTerm (x^2 + 1)","integrateBy x","antiDerivative FF"],
24.64 - ("Integrate.thy",["integrate","function"],
24.65 + ("Integrate",["integrate","function"],
24.66 ["diff","integration"]))];
24.67 Iterator 1;
24.68 moveActiveRoot 1;
24.69 @@ -486,17 +486,17 @@
24.70 srls = e_rls,
24.71 prls=e_rls,
24.72 crls = Atools_erls, nrls = e_rls},
24.73 -"Script IntegrationScript (f_::real) (v_::real) = \
24.74 -\ (((Rewrite_Set_Inst [(bdv,v_)] integration_rules False) @@ \
24.75 -\ (Rewrite_Set_Inst [(bdv,v_)] add_new_c False) @@ \
24.76 -\ (Rewrite_Set_Inst [(bdv,v_)] simplify_Integral False)) (f_::real))"
24.77 +"Script IntegrationScript (f_::real) (v_v::real) = \
24.78 +\ (((Rewrite_Set_Inst [(bdv,v_v)] integration_rules False) @@ \
24.79 +\ (Rewrite_Set_Inst [(bdv,v_v)] add_new_c False) @@ \
24.80 +\ (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) (f_::real))"
24.81 ));
24.82
24.83 states:=[];
24.84 CalcTree
24.85 [(["functionTerm (Integral x^2 + 1 D x)","integrateBy x",
24.86 "antiDerivative FF"],
24.87 - ("Integrate.thy",["integrate","function"],
24.88 + ("Integrate",["integrate","function"],
24.89 ["diff","integration","test"]))];
24.90 Iterator 1;
24.91 moveActiveRoot 1;
24.92 @@ -527,7 +527,7 @@
24.93 states:=[];
24.94 CalcTree
24.95 [(["functionTerm (x^2 + 1)","integrateBy x","antiDerivative FF"],
24.96 - ("Integrate.thy",["integrate","function"],
24.97 + ("Integrate",["integrate","function"],
24.98 ["diff","integration"]))];
24.99 Iterator 1;
24.100 moveActiveRoot 1;
25.1 --- a/test/Tools/isac/Knowledge/logexp.sml Wed Sep 08 16:45:27 2010 +0200
25.2 +++ b/test/Tools/isac/Knowledge/logexp.sml Wed Sep 08 16:47:22 2010 +0200
25.3 @@ -36,7 +36,7 @@
25.4
25.5 val fmz = ["equality ((2 log x) = 3)","solveFor x", "solutions L"];
25.6 val (dI',pI',mI') =
25.7 - ("Isac.thy",["logarithmic","univariate","equation","test"],
25.8 + ("Isac",["logarithmic","univariate","equation","test"],
25.9 ["Test","solve_log"]);
25.10 val p = e_pos'; val c = [];
25.11 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
26.1 --- a/test/Tools/isac/Knowledge/poly.sml Wed Sep 08 16:45:27 2010 +0200
26.2 +++ b/test/Tools/isac/Knowledge/poly.sml Wed Sep 08 16:47:22 2010 +0200
26.3 @@ -395,7 +395,7 @@
26.4 \- (3*x^^^5 + 8) * (6*x^^^4 - 1))",
26.5 "normalform N"];
26.6 val (dI',pI',mI') =
26.7 - ("Poly.thy",["polynomial","simplification"],
26.8 + ("Poly",["polynomial","simplification"],
26.9 ["simplification","for_polynomials"]);
26.10 val p = e_pos'; val c = [];
26.11 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
26.12 @@ -420,7 +420,7 @@
26.13 states:=[];
26.14 CalcTree
26.15 [(["TERM ((x - y)*(x + y))", "normalform N"],
26.16 - ("Poly.thy",["polynomial","simplification"],
26.17 + ("Poly",["polynomial","simplification"],
26.18 ["simplification","for_polynomials"]))];
26.19 Iterator 1;
26.20 moveActiveRoot 1;
27.1 --- a/test/Tools/isac/Knowledge/polyeq.sml Wed Sep 08 16:45:27 2010 +0200
27.2 +++ b/test/Tools/isac/Knowledge/polyeq.sml Wed Sep 08 16:47:22 2010 +0200
27.3 @@ -125,7 +125,7 @@
27.4 "----- d0_false ------";
27.5 (*EP*)
27.6 val fmz = ["equality ( 1 = 0)", "solveFor x","solutions L"];
27.7 -val (dI',pI',mI') = ("PolyEq.thy",["degree_0","polynomial","univariate","equation"],
27.8 +val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
27.9 ["PolyEq","solve_d0_polyeq_equation"]);
27.10 (*val p = e_pos';
27.11 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.12 @@ -143,7 +143,7 @@
27.13 "----- d0_true ------";
27.14 (*EP-7*)
27.15 val fmz = ["equality ( 0 = 0)", "solveFor x","solutions L"];
27.16 -val (dI',pI',mI') = ("PolyEq.thy",["degree_0","polynomial","univariate","equation"],
27.17 +val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
27.18 ["PolyEq","solve_d0_polyeq_equation"]);
27.19 (*val p = e_pos'; val c = [];
27.20 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.21 @@ -167,7 +167,7 @@
27.22
27.23 "----- d2_pqformula1 ------!!!!";
27.24 val fmz = ["equality (-2 +(-1)*x + x^^^2 = 0)", "solveFor x","solutions L"];
27.25 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
27.26 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
27.27 (*val p = e_pos'; val c = [];
27.28 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.29 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
27.30 @@ -194,7 +194,7 @@
27.31 "----- d2_pqformula1_neg ------";
27.32 (*EP-8*)
27.33 val fmz = ["equality ( 2 +(-1)*x + x^^^2 = 0)", "solveFor x","solutions L"];
27.34 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
27.35 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
27.36 (*val p = e_pos'; val c = [];
27.37 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.38 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
27.39 @@ -217,7 +217,7 @@
27.40
27.41 "----- d2_pqformula2 ------";
27.42 val fmz = ["equality (-2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
27.43 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
27.44 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
27.45 ["PolyEq","solve_d2_polyeq_pq_equation"]);
27.46 (*val p = e_pos'; val c = [];
27.47 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.48 @@ -237,7 +237,7 @@
27.49
27.50 "----- d2_pqformula2_neg ------";
27.51 val fmz = ["equality ( 2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
27.52 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
27.53 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
27.54 ["PolyEq","solve_d2_polyeq_pq_equation"]);
27.55 (*val p = e_pos'; val c = [];
27.56 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.57 @@ -258,7 +258,7 @@
27.58 "----- d2_pqformula3 ------";
27.59 (*EP-9*)
27.60 val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
27.61 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
27.62 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
27.63 ["PolyEq","solve_d2_polyeq_pq_equation"]);
27.64 (*val p = e_pos'; val c = [];
27.65 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.66 @@ -277,7 +277,7 @@
27.67
27.68 "----- d2_pqformula3_neg ------";
27.69 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
27.70 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
27.71 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
27.72 ["PolyEq","solve_d2_polyeq_pq_equation"]);
27.73 (*val p = e_pos'; val c = [];
27.74 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.75 @@ -297,7 +297,7 @@
27.76
27.77 "----- d2_pqformula4 ------";
27.78 val fmz = ["equality (-2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
27.79 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
27.80 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
27.81 ["PolyEq","solve_d2_polyeq_pq_equation"]);
27.82 (*val p = e_pos'; val c = [];
27.83 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.84 @@ -316,7 +316,7 @@
27.85
27.86 "----- d2_pqformula4_neg ------";
27.87 val fmz = ["equality ( 2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
27.88 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
27.89 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
27.90 ["PolyEq","solve_d2_polyeq_pq_equation"]);
27.91 (*val p = e_pos'; val c = [];
27.92 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.93 @@ -334,7 +334,7 @@
27.94
27.95 "----- d2_pqformula5 ------";
27.96 val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
27.97 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
27.98 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
27.99 ["PolyEq","solve_d2_polyeq_pq_equation"]);
27.100 (*val p = e_pos'; val c = [];
27.101 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.102 @@ -353,7 +353,7 @@
27.103
27.104 "----- d2_pqformula6 ------";
27.105 val fmz = ["equality (1*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
27.106 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
27.107 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
27.108 ["PolyEq","solve_d2_polyeq_pq_equation"]);
27.109 (*val p = e_pos'; val c = [];
27.110 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.111 @@ -373,7 +373,7 @@
27.112 "----- d2_pqformula7 ------";
27.113 (*EP-10*)
27.114 val fmz = ["equality ( x + x^^^2 = 0)", "solveFor x","solutions L"];
27.115 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
27.116 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
27.117 ["PolyEq","solve_d2_polyeq_pq_equation"]);
27.118 (*val p = e_pos'; val c = [];
27.119 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.120 @@ -392,7 +392,7 @@
27.121
27.122 "----- d2_pqformula8 ------";
27.123 val fmz = ["equality ( x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
27.124 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
27.125 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
27.126 ["PolyEq","solve_d2_polyeq_pq_equation"]);
27.127 (*val p = e_pos'; val c = [];
27.128 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.129 @@ -412,7 +412,7 @@
27.130
27.131 "----- d2_pqformula9 ------";
27.132 val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
27.133 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
27.134 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
27.135 ["PolyEq","solve_d2_polyeq_pq_equation"]);
27.136 (*val p = e_pos'; val c = [];
27.137 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.138 @@ -432,7 +432,7 @@
27.139
27.140 "----- d2_pqformula10_neg ------";
27.141 val fmz = ["equality (4 + x^^^2 = 0)", "solveFor x","solutions L"];
27.142 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
27.143 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
27.144 ["PolyEq","solve_d2_polyeq_pq_equation"]);
27.145 (*val p = e_pos'; val c = [];
27.146 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.147 @@ -452,7 +452,7 @@
27.148
27.149 "----- d2_pqformula10 ------";
27.150 val fmz = ["equality (-4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
27.151 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
27.152 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
27.153 ["PolyEq","solve_d2_polyeq_pq_equation"]);
27.154 (*val p = e_pos'; val c = [];
27.155 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.156 @@ -471,7 +471,7 @@
27.157
27.158 "----- d2_pqformula9_neg ------";
27.159 val fmz = ["equality (4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
27.160 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
27.161 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
27.162 ["PolyEq","solve_d2_polyeq_pq_equation"]);
27.163 (*val p = e_pos'; val c = [];
27.164 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.165 @@ -493,7 +493,7 @@
27.166 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
27.167
27.168 val fmz = ["equality (-1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
27.169 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
27.170 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
27.171 ["PolyEq","solve_d2_polyeq_abc_equation"]);
27.172 (*val p = e_pos'; val c = [];
27.173 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.174 @@ -511,7 +511,7 @@
27.175 | _ => raise error "polyeq.sml: diff.behav. in -1 + (-1)*x + 2*x^2 = 0 -> [x = 1, x = -1/2]";
27.176
27.177 val fmz = ["equality ( 1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
27.178 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
27.179 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
27.180 ["PolyEq","solve_d2_polyeq_abc_equation"]);
27.181 (*val p = e_pos'; val c = [];
27.182 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.183 @@ -530,7 +530,7 @@
27.184
27.185 (*EP-11*)
27.186 val fmz = ["equality (-1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
27.187 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
27.188 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
27.189 ["PolyEq","solve_d2_polyeq_abc_equation"]);
27.190 (*val p = e_pos'; val c = [];
27.191 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.192 @@ -548,7 +548,7 @@
27.193 | _ => raise error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]";
27.194
27.195 val fmz = ["equality ( 1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
27.196 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
27.197 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
27.198 ["PolyEq","solve_d2_polyeq_abc_equation"]);
27.199 (*val p = e_pos'; val c = [];
27.200 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.201 @@ -567,7 +567,7 @@
27.202 "TODO 1 + x + 2*x^^^2 = 0";
27.203
27.204 val fmz = ["equality (-2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
27.205 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
27.206 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
27.207 ["PolyEq","solve_d2_polyeq_abc_equation"]);
27.208 (*val p = e_pos'; val c = [];
27.209 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.210 @@ -585,7 +585,7 @@
27.211 | _ => raise error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]";
27.212
27.213 val fmz = ["equality ( 2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
27.214 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
27.215 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
27.216 ["PolyEq","solve_d2_polyeq_abc_equation"]);
27.217 (*val p = e_pos'; val c = [];
27.218 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.219 @@ -605,7 +605,7 @@
27.220
27.221 (*EP-12*)
27.222 val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
27.223 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
27.224 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
27.225 ["PolyEq","solve_d2_polyeq_abc_equation"]);
27.226 (*val p = e_pos'; val c = [];
27.227 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.228 @@ -623,7 +623,7 @@
27.229 | _ => raise error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]";
27.230
27.231 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
27.232 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
27.233 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
27.234 ["PolyEq","solve_d2_polyeq_abc_equation"]);
27.235 (*val p = e_pos'; val c = [];
27.236 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.237 @@ -643,7 +643,7 @@
27.238
27.239 (*EP-13*)
27.240 val fmz = ["equality (-8 + 2*x^^^2 = 0)", "solveFor x","solutions L"];
27.241 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
27.242 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
27.243 ["PolyEq","solve_d2_polyeq_abc_equation"]);
27.244 (*val p = e_pos'; val c = [];
27.245 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.246 @@ -661,7 +661,7 @@
27.247 | _ => raise error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]";
27.248
27.249 val fmz = ["equality ( 8+ 2*x^^^2 = 0)", "solveFor x","solutions L"];
27.250 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
27.251 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
27.252 ["PolyEq","solve_d2_polyeq_abc_equation"]);
27.253 (*val p = e_pos'; val c = [];
27.254 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.255 @@ -680,7 +680,7 @@
27.256
27.257 (*EP-14*)
27.258 val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
27.259 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
27.260 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
27.261 (*val p = e_pos'; val c = [];
27.262 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.263 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
27.264 @@ -698,7 +698,7 @@
27.265
27.266
27.267 val fmz = ["equality ( 4+ x^^^2 = 0)", "solveFor x","solutions L"];
27.268 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
27.269 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
27.270 (*val p = e_pos'; val c = [];
27.271 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.272 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
27.273 @@ -716,7 +716,7 @@
27.274
27.275 (*EP-15*)
27.276 val fmz = ["equality (2*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
27.277 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
27.278 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
27.279 ["PolyEq","solve_d2_polyeq_abc_equation"]);
27.280 (*val p = e_pos'; val c = [];
27.281 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.282 @@ -734,7 +734,7 @@
27.283 | _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
27.284
27.285 val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
27.286 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
27.287 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
27.288 ["PolyEq","solve_d2_polyeq_abc_equation"]);
27.289 (*val p = e_pos'; val c = [];
27.290 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.291 @@ -753,7 +753,7 @@
27.292
27.293 (*EP-16*)
27.294 val fmz = ["equality (x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
27.295 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
27.296 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
27.297 ["PolyEq","solve_d2_polyeq_abc_equation"]);
27.298 (*val p = e_pos'; val c = [];
27.299 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.300 @@ -772,7 +772,7 @@
27.301
27.302 (*EP-//*)
27.303 val fmz = ["equality (x + x^^^2 = 0)", "solveFor x","solutions L"];
27.304 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
27.305 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
27.306 ["PolyEq","solve_d2_polyeq_abc_equation"]);
27.307 (*val p = e_pos'; val c = [];
27.308 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.309 @@ -795,7 +795,7 @@
27.310 val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
27.311 "solveFor x","solutions L"];
27.312 val (dI',pI',mI') =
27.313 - ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
27.314 + ("PolyEq",["degree_2","expanded","univariate","equation"],
27.315 ["PolyEq","complete_square"]);
27.316 (* val p = e_pos'; val c = [];
27.317 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.318 @@ -806,7 +806,7 @@
27.319 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
27.320 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
27.321 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
27.322 - (*Apply_Method ("PolyEq.thy","complete_square")*)
27.323 + (*Apply_Method ("PolyEq","complete_square")*)
27.324 val (p,_,f,nxt,_,pt) = me nxt p c pt;
27.325 (*"-8 - 2 * x + x ^^^ 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
27.326 val (p,_,f,nxt,_,pt) = me nxt p c pt;
27.327 @@ -854,7 +854,7 @@
27.328 val fmz = ["equality (3 - 10*x + 3*x^^^2 = 0)",
27.329 "solveFor x","solutions L"];
27.330 val (dI',pI',mI') =
27.331 - ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
27.332 + ("PolyEq",["degree_2","expanded","univariate","equation"],
27.333 ["PolyEq","complete_square"]);
27.334 (* val p = e_pos'; val c = [];
27.335 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.336 @@ -868,7 +868,7 @@
27.337 val (p,_,f,nxt,_,pt) = me nxt p c pt;
27.338 val (p,_,f,nxt,_,pt) = me nxt p c pt;
27.339 val (p,_,f,nxt,_,pt) = me nxt p c pt;
27.340 - (*Apply_Method ("PolyEq.thy","complete_square")*)
27.341 + (*Apply_Method ("PolyEq","complete_square")*)
27.342 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
27.343
27.344 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
27.345 @@ -877,7 +877,7 @@
27.346 val fmz = ["equality (-16 + 4*x + 2*x^^^2 = 0)",
27.347 "solveFor x","solutions L"];
27.348 val (dI',pI',mI') =
27.349 - ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
27.350 + ("PolyEq",["degree_2","expanded","univariate","equation"],
27.351 ["PolyEq","complete_square"]);
27.352 (* val p = e_pos'; val c = [];
27.353 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.354 @@ -891,7 +891,7 @@
27.355 val (p,_,f,nxt,_,pt) = me nxt p c pt;
27.356 val (p,_,f,nxt,_,pt) = me nxt p c pt;
27.357 val (p,_,f,nxt,_,pt) = me nxt p c pt;
27.358 - (*Apply_Method ("PolyEq.thy","complete_square")*)
27.359 + (*Apply_Method ("PolyEq","complete_square")*)
27.360 val (p,_,f,nxt,_,pt) = me nxt p c pt;
27.361 val (p,_,f,nxt,_,pt) = me nxt p c pt;
27.362 val (p,_,f,nxt,_,pt) = me nxt p c pt;
27.363 @@ -913,7 +913,7 @@
27.364 val fmz = ["equality (a*b - (a+b)*x + x^^^2 = 0)",
27.365 "solveFor x","solutions L"];
27.366 val (dI',pI',mI') =
27.367 - ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
27.368 + ("PolyEq",["degree_2","expanded","univariate","equation"],
27.369 ["PolyEq","complete_square"]);
27.370 (* val p = e_pos'; val c = [];
27.371 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.372 @@ -956,7 +956,7 @@
27.373 val fmz = ["equality (-64 + x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.a~*)
27.374 "solveFor x","solutions L"];
27.375 val (dI',pI',mI') =
27.376 - ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
27.377 + ("PolyEq",["degree_2","expanded","univariate","equation"],
27.378 ["PolyEq","complete_square"]);
27.379 (* val p = e_pos'; val c = [];
27.380 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.381 @@ -987,7 +987,7 @@
27.382 val fmz = ["equality (-147 + 3*x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.b*)
27.383 "solveFor x","solutions L"];
27.384 val (dI',pI',mI') =
27.385 - ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
27.386 + ("PolyEq",["degree_2","expanded","univariate","equation"],
27.387 ["PolyEq","complete_square"]);
27.388 (* val p = e_pos'; val c = [];
27.389 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.390 @@ -1017,7 +1017,7 @@
27.391 val fmz = ["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"];
27.392 (* refine fmz ["univariate","equation"];
27.393 *)
27.394 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
27.395 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
27.396 (*val p = e_pos';
27.397 val c = [];
27.398 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.399 @@ -1036,7 +1036,7 @@
27.400 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
27.401 (* val nxt =
27.402 ("Subproblem",
27.403 - Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))
27.404 + Subproblem ("PolyEq",["polynomial","univariate","equation"]))
27.405 : string * tac *)
27.406 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
27.407 (*val nxt =
27.408 @@ -1061,7 +1061,7 @@
27.409 (*is in rlang.sml, too*)
27.410 val fmz = ["equality ((x+1)*(x+2) - (3*x - 2)^^^2=(2*x - 1)^^^2+(3*x - 1)*(x+1))",
27.411 "solveFor x","solutions L"];
27.412 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
27.413 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
27.414
27.415 (*val p = e_pos'; val c = [];
27.416 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.417 @@ -1082,7 +1082,7 @@
27.418 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
27.419 (* val nxt =
27.420 ("Subproblem",
27.421 - Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))
27.422 + Subproblem ("PolyEq",["polynomial","univariate","equation"]))
27.423 : string * tac*)
27.424 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
27.425 (*val nxt =
27.426 @@ -1106,7 +1106,7 @@
27.427 val fmz = ["equality ( -4 + x^^^2 =0)", "solveFor x","solutions L"];
27.428 (* val fmz = ["equality (1 + x^^^2 =0)", "solveFor x","solutions L"];*)
27.429 (*val fmz = ["equality (0 =0)", "solveFor x","solutions L"];*)
27.430 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
27.431 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
27.432 (*val p = e_pos';
27.433 val c = [];
27.434 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
27.435 @@ -1169,7 +1169,7 @@
27.436 states:=[];
27.437 CalcTree
27.438 [(["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"],
27.439 - ("PolyEq.thy",["univariate","equation"],["no_met"]))];
27.440 + ("PolyEq",["univariate","equation"],["no_met"]))];
27.441 Iterator 1;
27.442 moveActiveRoot 1;
27.443 autoCalculate 1 CompleteCalc;
28.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Wed Sep 08 16:45:27 2010 +0200
28.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Wed Sep 08 16:47:22 2010 +0200
28.3 @@ -252,7 +252,7 @@
28.4 states:=[];
28.5 CalcTree [(["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
28.6 "normalform N"],
28.7 - ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
28.8 + ("PolyMinus",["plus_minus","polynom","vereinfachen"],
28.9 ["simplification","for_polynomials","with_minus"]))];
28.10 moveActiveRoot 1;
28.11 autoCalculate 1 CompleteCalc;
28.12 @@ -265,7 +265,7 @@
28.13 states:=[];
28.14 CalcTree [(["TERM (-r - 2*s - 3*t + 5 + 4*r + 8*s - 5*t - 2)",
28.15 "normalform N"],
28.16 - ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
28.17 + ("PolyMinus",["plus_minus","polynom","vereinfachen"],
28.18 ["simplification","for_polynomials","with_minus"]))];
28.19 moveActiveRoot 1;
28.20 autoCalculate 1 CompleteCalc;
28.21 @@ -279,7 +279,7 @@
28.22 states:=[];
28.23 CalcTree [(["TERM (3*e - 6*f - 8*e - 4*f + 5*e + 7*f)",
28.24 "normalform N"],
28.25 - ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
28.26 + ("PolyMinus",["plus_minus","polynom","vereinfachen"],
28.27 ["simplification","for_polynomials","with_minus"]))];
28.28 moveActiveRoot 1;
28.29 autoCalculate 1 CompleteCalc;
28.30 @@ -292,7 +292,7 @@
28.31 states:=[];
28.32 CalcTree [(["TERM (8*u - 5*v - 5*u + 7*v - 6*u - 3*v)",
28.33 "normalform N"],
28.34 - ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
28.35 + ("PolyMinus",["plus_minus","polynom","vereinfachen"],
28.36 ["simplification","for_polynomials","with_minus"]))];
28.37 moveActiveRoot 1;
28.38 autoCalculate 1 CompleteCalc;
28.39 @@ -305,7 +305,7 @@
28.40 states:=[];
28.41 CalcTree [(["TERM (2*u - 3*v - 6*u + 5*v)",
28.42 "normalform N"],
28.43 - ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
28.44 + ("PolyMinus",["plus_minus","polynom","vereinfachen"],
28.45 ["simplification","for_polynomials","with_minus"]))];
28.46 moveActiveRoot 1;
28.47 autoCalculate 1 CompleteCalc;
28.48 @@ -320,7 +320,7 @@
28.49 "----------- met probe fuer_polynom ------------------------------";
28.50 val str =
28.51 "Script ProbeScript (e_e::bool) (ws_::bool list) =\
28.52 -\ (let e_e = Take e_; \
28.53 +\ (let e_e = Take e_e; \
28.54 \ e_e = Substitute ws_ e_e \
28.55 \ in (Repeat((Try (Repeat (Calculate TIMES))) @@ \
28.56 \ (Try (Repeat (Calculate PLUS ))) @@ \
28.57 @@ -337,7 +337,7 @@
28.58 \3 - 2 * e + 2 * f + 2 * g)",
28.59 "mitWert [e = 1, f = 2, g = 3]",
28.60 "Geprueft b"],
28.61 - ("PolyMinus.thy",["polynom","probe"],
28.62 + ("PolyMinus",["polynom","probe"],
28.63 ["probe","fuer_polynom"]))];
28.64 moveActiveRoot 1;
28.65 autoCalculate 1 CompleteCalc;
28.66 @@ -359,7 +359,7 @@
28.67 states:=[];
28.68 CalcTree [(["TERM (2*u - 5 - (3 - 4*u) + (8*u + 9))",
28.69 "normalform N"],
28.70 - ("PolyMinus.thy",["klammer","polynom","vereinfachen"],
28.71 + ("PolyMinus",["klammer","polynom","vereinfachen"],
28.72 ["simplification","for_polynomials","with_parentheses"]))];
28.73 moveActiveRoot 1;
28.74 autoCalculate 1 CompleteCalc;
28.75 @@ -374,7 +374,7 @@
28.76 CalcTree [(["Pruefe (2*u - 5 - (3 - 4*u) + (8*u + 9) = 1 + 14 * u)",
28.77 "mitWert [u = 2]",
28.78 "Geprueft b"],
28.79 - ("PolyMinus.thy",["polynom","probe"],
28.80 + ("PolyMinus",["polynom","probe"],
28.81 ["probe","fuer_polynom"]))];
28.82 moveActiveRoot 1;
28.83 autoCalculate 1 CompleteCalc;
28.84 @@ -390,7 +390,7 @@
28.85 states:=[];
28.86 CalcTree [(["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
28.87 "normalform N"],
28.88 - ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
28.89 + ("PolyMinus",["plus_minus","polynom","vereinfachen"],
28.90 ["simplification","for_polynomials","with_minus"]))];
28.91 moveActiveRoot 1;
28.92 autoCalculate 1 CompleteCalcHead;
28.93 @@ -450,7 +450,7 @@
28.94 states:=[];
28.95 CalcTree [(["TERM (- (8 * g) + 10 * g + h)",
28.96 "normalform N"],
28.97 - ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
28.98 + ("PolyMinus",["plus_minus","polynom","vereinfachen"],
28.99 ["simplification","for_polynomials","with_minus"]))];
28.100 moveActiveRoot 1;
28.101 autoCalculate 1 CompleteCalc;
28.102 @@ -462,7 +462,7 @@
28.103 states:=[];
28.104 CalcTree [(["TERM (- (8 * g) + 10 * g + f)",
28.105 "normalform N"],
28.106 - ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
28.107 + ("PolyMinus",["plus_minus","polynom","vereinfachen"],
28.108 ["simplification","for_polynomials","with_minus"]))];
28.109 moveActiveRoot 1;
28.110 autoCalculate 1 CompleteCalc;
28.111 @@ -511,7 +511,7 @@
28.112 states:=[];
28.113 CalcTree [(["TERM ((3*a + 2) * (4*a - 1))",
28.114 "normalform N"],
28.115 - ("PolyMinus.thy",["binom_klammer","polynom","vereinfachen"],
28.116 + ("PolyMinus",["binom_klammer","polynom","vereinfachen"],
28.117 ["simplification","for_polynomials","with_parentheses_mult"]))];
28.118 moveActiveRoot 1;
28.119 autoCalculate 1 CompleteCalc;
28.120 @@ -530,7 +530,7 @@
28.121 states:=[];
28.122 CalcTree [(["TERM (8*(a - q) + a - 2*q + 3*(a - 2*q))",
28.123 "normalform N"],
28.124 - ("PolyMinus.thy",["binom_klammer","polynom","vereinfachen"],
28.125 + ("PolyMinus",["binom_klammer","polynom","vereinfachen"],
28.126 ["simplification","for_polynomials","with_parentheses_mult"]))];
28.127 moveActiveRoot 1;
28.128 autoCalculate 1 CompleteCalc;
29.1 --- a/test/Tools/isac/Knowledge/rateq.sml Wed Sep 08 16:45:27 2010 +0200
29.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Wed Sep 08 16:47:22 2010 +0200
29.3 @@ -46,7 +46,7 @@
29.4 (* refine fmz ["univariate","equation"];
29.5 *)
29.6
29.7 -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
29.8 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
29.9 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
29.10 (* val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
29.11 --------------------------------------- Refine_Tacitly*)
29.12 @@ -56,7 +56,7 @@
29.13 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
29.14 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
29.15 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
29.16 -(* val nxt = ("Subproblem",Subproblem ("RatEq.thy",["univariate","equation"])*)
29.17 +(* val nxt = ("Subproblem",Subproblem ("RatEq",["univariate","equation"])*)
29.18 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
29.19 (* val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
29.20 --------------------------------------- Refine_Tacitly*)
29.21 @@ -73,7 +73,7 @@
29.22 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
29.23 (**** assoc_thm': 'all_left' not in 'RatEq.thy' (and parents)*)
29.24 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
29.25 -(* val nxt = ("Subproblem", Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
29.26 +(* val nxt = ("Subproblem", Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)
29.27
29.28
29.29
29.30 @@ -104,7 +104,7 @@
29.31 (* refine fmz ["univariate","equation"];
29.32 *)
29.33
29.34 -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
29.35 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
29.36 (*val p = e_pos';
29.37 val c = [];
29.38 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
29.39 @@ -118,7 +118,7 @@
29.40 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
29.41 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
29.42 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
29.43 -(* nxt = ("Subproblem",Subproblem ("RatEq.thy",["univariate","equation"]))*)
29.44 +(* nxt = ("Subproblem",Subproblem ("RatEq",["univariate","equation"]))*)
29.45 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
29.46 (* nxt = ("Model_Problem", Model_Problem ["normalize","polynomial","univariate","equation"])*)
29.47 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
29.48 @@ -127,7 +127,7 @@
29.49 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
29.50 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
29.51 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
29.52 -(* ("Subproblem", Subproblem ("PolyEq.thy",["polynomial","univariate","equation"])) *)
29.53 +(* ("Subproblem", Subproblem ("PolyEq",["polynomial","univariate","equation"])) *)
29.54 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
29.55 (* nxt = ("Model_Problem", Model_Problem
29.56 ["abcFormula","degree_2","polynomial","univariate","equation"])*)
30.1 --- a/test/Tools/isac/Knowledge/rational-old.sml Wed Sep 08 16:45:27 2010 +0200
30.2 +++ b/test/Tools/isac/Knowledge/rational-old.sml Wed Sep 08 16:47:22 2010 +0200
30.3 @@ -242,7 +242,7 @@
30.4 val (t,asm) = the (rewrite_set_ thy eval_rls false rls t);
30.5
30.6
30.7 -val thy' = "Rational.thy";
30.8 +val thy' = "Rational";
30.9 val rls' = "cancel";
30.10 val t' = "(1 + 1 * a ^^^ 1)///(-2 + 2 * a ^^^ 2)";
30.11 val (t',asm') = the (rewrite_set thy' "eval_rls" false rls' t');
30.12 @@ -250,12 +250,12 @@
30.13 else raise error "tests/rationals.sml(1): new behaviour";*)
30.14
30.15
30.16 -val thy' = "Rational.thy";
30.17 +val thy' = "Rational";
30.18 val rls' = "cancel";
30.19 val t' = "(10 * a^^^2 * b * c + 14 * a * b + 3 * a * c + 20 * a * b^^^2 * c) /// (5 * a * b * c + 7 * a^^^2 * b * c) ";
30.20 val (t',asm') = the (rewrite_set thy' "eval_rls" false rls' t');
30.21
30.22 -val thy' = "Rational.thy";
30.23 +val thy' = "Rational";
30.24 val rls' = "cancel";
30.25 val t' = "(a^^^2 * b + 2 * a * b + b ) /// ( a^^^2 - 1 )";
30.26 val (t',asm') = the (rewrite_set thy' "eval_rls" false rls' t');
30.27 @@ -274,7 +274,7 @@
30.28 Schalk
30.29 Reniets Verlag *)
30.30
30.31 -val thy' = "Rational.thy";
30.32 +val thy' = "Rational";
30.33 val rls' = "cancel";
30.34 val mp = "make_polynomial";
30.35
31.1 --- a/test/Tools/isac/Knowledge/rational.sml Wed Sep 08 16:45:27 2010 +0200
31.2 +++ b/test/Tools/isac/Knowledge/rational.sml Wed Sep 08 16:47:22 2010 +0200
31.3 @@ -472,7 +472,7 @@
31.4 "-------- cancel from: Mathematik 1 Schalk Reniets Verlag --------";
31.5 "-------- cancel from: Mathematik 1 Schalk Reniets Verlag --------";
31.6 "-------- cancel from: Mathematik 1 Schalk Reniets Verlag --------";
31.7 -val thy' = "Rational.thy";
31.8 +val thy' = "Rational";
31.9 val rls' = "cancel";
31.10 val mp = "make_polynomial";
31.11
31.12 @@ -1828,7 +1828,7 @@
31.13 val fmz = ["TERM ((14 * x * y) / ( x * y ))",
31.14 "normalform N"];
31.15 val (dI',pI',mI') =
31.16 - ("Rational.thy",["rational","simplification"],
31.17 + ("Rational",["rational","simplification"],
31.18 ["simplification","of_rationals"]);
31.19 val p = e_pos'; val c = [];
31.20 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
31.21 @@ -1854,7 +1854,7 @@
31.22 states:=[];
31.23 CalcTree
31.24 [(["TERM (((2 - x)/(2*a)) / (2*a/(x - 2)))", "normalform N"],
31.25 - ("Rational.thy",["rational","simplification"],
31.26 + ("Rational",["rational","simplification"],
31.27 ["simplification","of_rationals"]))];
31.28 Iterator 1;
31.29 moveActiveRoot 1;
31.30 @@ -1871,7 +1871,7 @@
31.31 states:=[];
31.32 CalcTree
31.33 [(["TERM ((a^2 + -1*b^2) / (a^2 + -2*a*b + b^2))", "normalform N"],
31.34 - ("Rational.thy",["rational","simplification"],
31.35 + ("Rational",["rational","simplification"],
31.36 ["simplification","of_rationals"]))];
31.37 Iterator 1;
31.38 moveActiveRoot 1;
32.1 --- a/test/Tools/isac/Knowledge/rlang.sml Wed Sep 08 16:45:27 2010 +0200
32.2 +++ b/test/Tools/isac/Knowledge/rlang.sml Wed Sep 08 16:47:22 2010 +0200
32.3 @@ -57,7 +57,7 @@
32.4 (*EP*)
32.5 val fmz = ["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)",
32.6 "solveFor x","solutions L"];
32.7 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
32.8 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
32.9 (*val p = e_pos';
32.10 val c = [];
32.11 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
32.12 @@ -88,7 +88,7 @@
32.13 (*EP*)
32.14 val fmz = ["equality ((x - 5)*(10 - x) = (3 - x)*(2 + x) + 2*(x + 20))",
32.15 "solveFor x","solutions L"];
32.16 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
32.17 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
32.18 (*val p = e_pos';
32.19 val c = [];
32.20 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
32.21 @@ -118,7 +118,7 @@
32.22 (*EP*)
32.23 val fmz = ["equality ((2*x+5)^^^2+(3*x+4)^^^2=(13*x+2)*(x+1)+2*(15+14*x))",
32.24 "solveFor x","solutions L"];
32.25 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
32.26 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
32.27 (*val p = e_pos';
32.28 val c = [];
32.29 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
32.30 @@ -148,7 +148,7 @@
32.31 (*EP*)
32.32 val fmz = ["equality ((2*x+1)^^^3+(x+1)^^^3=(2*x+1)^^^2*2*x+(x+2)^^^3+x^^^2)",
32.33 "solveFor x","solutions L"];
32.34 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
32.35 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
32.36 (*val p = e_pos';
32.37 val c = [];
32.38 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
32.39 @@ -178,7 +178,7 @@
32.40 (*ER-2*)
32.41 val fmz = ["equality ((3*x+5)/18 - x/2 = -((3*x - 2)/9))",
32.42 "solveFor x","solutions L"];
32.43 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
32.44 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
32.45 (*val p = e_pos'; val c = [];
32.46 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
32.47 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
32.48 @@ -220,7 +220,7 @@
32.49 (*ER-1*)
32.50 val fmz = ["equality ((17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0)",
32.51 "solveFor x","solutions L"];
32.52 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
32.53 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
32.54 (*val p = e_pos';
32.55 val c = [];
32.56 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
32.57 @@ -260,7 +260,7 @@
32.58 (*ER-3*)
32.59 val fmz = ["equality (-2/x + 3/(2*x) - 4/(3*x) + 5/(4*x) + 6/(5*x) = 65/8)",
32.60 "solveFor x","solutions L"];
32.61 -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
32.62 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
32.63 (*val p = e_pos';
32.64 val c = [];
32.65 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
32.66 @@ -300,7 +300,7 @@
32.67 (*ER-4*)
32.68 val fmz = ["equality ((x+3)/(2*x - 4)=3)",
32.69 "solveFor x","solutions L"];
32.70 -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
32.71 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
32.72 (*val p = e_pos';
32.73 val c = [];
32.74 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
32.75 @@ -342,7 +342,7 @@
32.76 (*ER-5*)
32.77 val fmz = ["equality ((1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 = -1*(6*x)^^^2 + 29)",
32.78 "solveFor x","solutions L"];
32.79 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
32.80 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
32.81 (*val p = e_pos';
32.82 val c = [];
32.83 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
32.84 @@ -388,7 +388,7 @@
32.85 (*ER-6*)
32.86 val fmz = ["equality ((5*x)/(x - 2) - x/(x+2)=4)",
32.87 "solveFor x","solutions L"];
32.88 -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
32.89 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
32.90 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
32.91 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.92 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.93 @@ -425,7 +425,7 @@
32.94 (*ER-7*)
32.95 val fmz = ["equality (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)",
32.96 "solveFor x","solutions L"];
32.97 -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
32.98 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
32.99 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
32.100 (*val nxt = ("Model_Problem",Model_Problem["rational","univariate","equation"*)
32.101 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.102 @@ -445,7 +445,7 @@
32.103 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.104 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.105 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; 040209 MGs norm_Rational*)
32.106 -(* val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"])*)
32.107 +(* val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"])*)
32.108 if f= Form' (FormKF (~1, EdUndef, 0, Nundef, "-6 * x + 5 * x ^^^ 2 = 0"))then()
32.109 else raise error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b";
32.110 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.111 @@ -511,7 +511,7 @@
32.112 (*ER-8*)
32.113 val fmz = ["equality (((x - 1)/(x+1)+1)/((x - 1)/(x+1) - (x+1)/(x - 1))=2)",
32.114 "solveFor x","solutions L"];
32.115 -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
32.116 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
32.117
32.118 (*val p = e_pos'; val c = [];
32.119 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
32.120 @@ -551,7 +551,7 @@
32.121 (*ER-10*)
32.122 val fmz = ["equality (m1*v1+m2*v2=0)",
32.123 "solveFor m1","solutions L"];
32.124 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
32.125 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
32.126
32.127 (*val p = e_pos'; val c = [];
32.128 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
32.129 @@ -580,7 +580,7 @@
32.130 (*ER-11*)
32.131 val fmz = ["equality (f=((w+u)/(w+v))*v0)",
32.132 "solveFor v","solutions L"];
32.133 -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
32.134 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
32.135
32.136 (*val p = e_pos'; val c = [];
32.137 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
32.138 @@ -595,7 +595,7 @@
32.139 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.140 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.141 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.142 -(*nxt = Subproblem ("RatEq.thy",["univariate","equation"])) *)
32.143 +(*nxt = Subproblem ("RatEq",["univariate","equation"])) *)
32.144 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.145 (*val nxt =Model_Problem ["normalize","polynomial","univariate","equation"])*)
32.146 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.147 @@ -605,7 +605,7 @@
32.148 (*val nxt = ("Apply_Method",Apply_Method ["PolyEq","normalize_poly"])*)
32.149 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.150 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.151 -(*val nxt =Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
32.152 +(*val nxt =Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)
32.153 if f = Form'
32.154 (FormKF
32.155 (~1,
32.156 @@ -659,7 +659,7 @@
32.157 (*ER-12*)
32.158 val fmz = ["equality (f=((w+u)/(w+v))*v0)",
32.159 "solveFor w","solutions L"];
32.160 -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
32.161 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
32.162 (*val p = e_pos';val c = [];
32.163 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
32.164 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
32.165 @@ -707,7 +707,7 @@
32.166 (*ER-9*)
32.167 val fmz = ["equality (1/R=1/R1+1/R2)",
32.168 "solveFor R1","solutions L"];
32.169 -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
32.170 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
32.171 (*val p = e_pos'; val c = [];
32.172 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
32.173 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
32.174 @@ -752,7 +752,7 @@
32.175 (*ER-13 + EO-11 ?!?*)
32.176 val fmz = ["equality (y^^^2=2*p*x)",
32.177 "solveFor p","solutions L"];
32.178 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
32.179 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
32.180 (*val p = e_pos'; val c = [];
32.181 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
32.182 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
32.183 @@ -785,7 +785,7 @@
32.184 (*EO ??*)
32.185 val fmz = ["equality (y^^^2=2*p*x)",
32.186 "solveFor y","solutions L"];
32.187 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
32.188 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
32.189 (*val p = e_pos';
32.190 val c = [];
32.191 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
32.192 @@ -818,7 +818,7 @@
32.193 (*EO-8*)
32.194 val fmz = ["equality (b^^^2*x^^^2 + a^^^2*y^^^2 = a^^^2*b^^^2)",
32.195 "solveFor x","solutions L"];
32.196 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
32.197 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
32.198 (*val p = e_pos';
32.199 val c = [];
32.200 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
32.201 @@ -868,7 +868,7 @@
32.202 (*ER-14*)
32.203 val fmz = ["equality (A = (1/2)*(x1*(y2 - y3)+x2*(y3 - y1)+x3*(y1 - y2)))",
32.204 "solveFor x2","solutions L"];
32.205 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
32.206 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
32.207 (*val p = e_pos';
32.208 val c = [];
32.209 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
32.210 @@ -907,7 +907,7 @@
32.211 (*EO*)
32.212 val fmz = ["equality (4*sqrt(4*x+1)=3*sqrt(7*x+2))",
32.213 "solveFor x","solutions L"];
32.214 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
32.215 +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
32.216 (*val p = e_pos';
32.217 val c = [];
32.218 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
32.219 @@ -945,7 +945,7 @@
32.220 "Schalk II s.56 Bsp 68a (5*sqrt(x) - 1 = 7*sqrt(x) - 5)";
32.221 val fmz = ["equality (5*sqrt(x) - 1 = 7*sqrt(x) - 5)",
32.222 "solveFor x","solutions L"];
32.223 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
32.224 +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
32.225 (*val p = e_pos';
32.226 val c = [];
32.227 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
32.228 @@ -1028,7 +1028,7 @@
32.229 (*EO-2*)
32.230 val fmz = ["equality (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))",
32.231 "solveFor x","solutions L"];
32.232 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
32.233 +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
32.234
32.235 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
32.236 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.237 @@ -1039,7 +1039,7 @@
32.238 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.239 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.240 (*"13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"
32.241 --> Subproblem ("RootEq.thy", ["univariate", ...])*)
32.242 +-> Subproblem ("RootEq", ["univariate", ...])*)
32.243 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.244 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.245 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.246 @@ -1048,7 +1048,7 @@
32.247 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.248 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.249 (*"144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"
32.250 --> Subproblem ("RootEq.thy", ["univariate", ...])*)
32.251 +-> Subproblem ("RootEq", ["univariate", ...])*)
32.252 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.253 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.254 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.255 @@ -1078,7 +1078,7 @@
32.256 (*EO-3*)
32.257 val fmz = ["equality (sqrt(4*x+1) - sqrt(x+3) = sqrt(x - 2))",
32.258 "solveFor x","solutions L"];
32.259 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
32.260 +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
32.261
32.262 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
32.263 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.264 @@ -1089,7 +1089,7 @@
32.265 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.266 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.267 (*4 + 5 * x + -2 * sqrt (3 + 13 * x + 4 * x ^^^ 2) = -2 + x"
32.268 --> Subproblem ("RootEq.thy", ["univariate", ...])*)
32.269 +-> Subproblem ("RootEq", ["univariate", ...])*)
32.270 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.271 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.272 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.273 @@ -1099,7 +1099,7 @@
32.274 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.275 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.276 (*"12 + 52 * x + 16 * x ^^^ 2 = 36 + x ^^^ 2 + 48 * x + 15 * x ^^^ 2"
32.277 --> Subproblem ("RootEq.thy", ["univariate", ...])*)
32.278 +-> Subproblem ("RootEq", ["univariate", ...])*)
32.279 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.280 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.281 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.282 @@ -1108,7 +1108,7 @@
32.283 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.284 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-24 + 4 * x = 0")) then ()
32.285 else raise error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 74a";
32.286 -(*-> ubproblem ("PolyEq.thy", ["degree_1", ...]*)
32.287 +(*-> ubproblem ("PolyEq", ["degree_1", ...]*)
32.288 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.289 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.290 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.291 @@ -1130,7 +1130,7 @@
32.292 (*EO-4*)
32.293 val fmz = ["equality (sqrt(x+12)+sqrt(x - 3) = sqrt(x + 32) - sqrt(5+x))",
32.294 "solveFor x","solutions L"];
32.295 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
32.296 +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
32.297
32.298 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
32.299 (* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"]) *)
32.300 @@ -1193,7 +1193,7 @@
32.301 (*EP*)
32.302 val fmz = ["equality ((6*x - 9)*(5*x+7) - (4*x+7)*(3*x - 6) = 429)",
32.303 "solveFor x","solutions L"];
32.304 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
32.305 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
32.306 (*val p = e_pos';
32.307 val c = [];
32.308 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
32.309 @@ -1222,7 +1222,7 @@
32.310 (*ER-15*)
32.311 val fmz = ["equality ((x - 4)/(x+4) = (1 - x)/(1+x))",
32.312 "solveFor x","solutions L"];
32.313 -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
32.314 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
32.315
32.316 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
32.317 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.318 @@ -1233,7 +1233,7 @@
32.319 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.320 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;
32.321 (*"(-4 + x) * (1 + x) = (1 + -1 * x) * (4 + x)"
32.322 --> Subproblem ("RatEq.thy", ["univariate", ...])*)
32.323 +-> Subproblem ("RatEq", ["univariate", ...])*)
32.324 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.325 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.326 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.327 @@ -1243,7 +1243,7 @@
32.328 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.329 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-8 + 2 * x ^^^ 2 = 0")) then ()
32.330 else raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 8a";
32.331 -(*-> Subproblem ("PolyEq.thy", ["polynomial", ...])*)
32.332 +(*-> Subproblem ("PolyEq", ["polynomial", ...])*)
32.333 (*
32.334 val Form' (FormKF (~1, EdUndef, 0, Nundef, str)) = f;
32.335 *)
32.336 @@ -1265,7 +1265,7 @@
32.337 "Schalk II s.66 Bsp 10b (1/(x^^^2 - 9)+(2*x+3)/(x+3)=(3*x+4)/(x - 3))";
32.338 val fmz = ["equality (1/(x^^^2 - 9)+(2*x+3)/(x+3)=(3*x+4)/(x - 3))",
32.339 "solveFor x","solutions L"];
32.340 -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
32.341 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
32.342 (*val p = e_pos';
32.343 val c = [];
32.344 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
32.345 @@ -1307,7 +1307,7 @@
32.346 "Schalk II s.66 Bsp 20a (sqrt(29 - sqrt (x^^^2 - 9))=5)";
32.347 val fmz = ["equality (sqrt(29 - sqrt(x^^^2 - 9))=5)",
32.348 "solveFor x","solutions L"];
32.349 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
32.350 +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
32.351 (*val p = e_pos';
32.352 val c = [];
32.353 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
32.354 @@ -1358,7 +1358,7 @@
32.355 *)
32.356 val fmz = ["equality (2*sqrt(261 - x) - sqrt(2+2*x)=sqrt(2)*sqrt(5 - 3*x))",
32.357 "solveFor x","solutions L"];
32.358 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
32.359 +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
32.360
32.361 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
32.362 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.363 @@ -1401,7 +1401,7 @@
32.364 "Schalk II s.66 Bsp 28a (A=(c/d)*sqrt(4*a^^^2 - c^^^2))";
32.365 val fmz = ["equality (A=(c/d)*sqrt(4*a^^^2 - c^^^2))",
32.366 "solveFor a","solutions L"];
32.367 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
32.368 +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
32.369 (*val p = e_pos';
32.370 val c = [];
32.371 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
32.372 @@ -1446,23 +1446,23 @@
32.373 "Schalk II s.68 Bsp 52b (1/(x - a+b)=1/x - 1/a + 1/b)";
32.374 val fmz = ["equality (1/(x - a+b)=1/x - 1/a + 1/b)",
32.375 "solveFor x","solutions L"];
32.376 -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
32.377 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
32.378 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
32.379 (* val nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"])*)
32.380 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.381 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.382 -(*val nxt = ("Specify_Theory",Specify_Theory "RatEq.thy")*)
32.383 +(*val nxt = ("Specify_Theory",Specify_Theory "RatEq")*)
32.384 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.385 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.386 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.387 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.388 (*val p = ([3],Res)
32.389 val f="1 * (a * (b * x)) = (a * b + (a * x + -1 * (b * x))) * (b + (x + -1 * a)
32.390 -val nxt = Subproblem ("RatEq.thy",["univariate","equation"]))*)
32.391 +val nxt = Subproblem ("RatEq",["univariate","equation"]))*)
32.392 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.393 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.394 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.395 -(*val nxt = ("Specify_Theory",Specify_Theory "PolyEq.thy")*)
32.396 +(*val nxt = ("Specify_Theory",Specify_Theory "PolyEq")*)
32.397 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.398 (* nxt = Specify_Problem ["normalize","polynomial","univariate","equation"])*)
32.399 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.400 @@ -1471,7 +1471,7 @@
32.401 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.402 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; at introducing of MGs norm_Rational*)
32.403 (*val p = ([4,5],Res) val f ="b * a ^^^ 2 + -1 * a * b ^^^ 2 + (a ^^^ 2 + b ^^^ 2 + -2 * a * b) * x +\n(b + -1 * a) * x ^^^ 2 =\n0"))
32.404 -val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
32.405 +val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)
32.406 if f = Form'
32.407 (FormKF
32.408 (~1,
32.409 @@ -1483,7 +1483,7 @@
32.410 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.411 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.412 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.413 -(*val nxt = ("Specify_Theory",Specify_Theory "PolyEq.thy")*)
32.414 +(*val nxt = ("Specify_Theory",Specify_Theory "PolyEq")*)
32.415 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.416 (*Specify_Problem["abcFormula","degree_2","polynomial","univariate","equation*)
32.417 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.418 @@ -1507,7 +1507,7 @@
32.419 (*----------------- Schalk II s.68 Bsp 56a ------------------------*)
32.420 "Schalk II s.68 Bsp 56a ((a+b*x)/(a-b*x) - (a - b*x)/(a+b*x)= (4*a*b)/(a^^^2 - b^^^2))";
32.421 val fmz = ["equality ((a+b*x)/(a-b*x) - (a - b*x)/(a+b*x)= (4*a*b)/(a^^^2 - b^^^2))","solveFor x","solutions L"];
32.422 -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
32.423 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
32.424 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
32.425 (* val nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"]) *)
32.426 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.427 @@ -1595,7 +1595,7 @@
32.428 "Schalk II s.68 Bsp 61b (sqrt(x+a)+sqrt(b - x)=sqrt(a+b))";
32.429 val fmz = ["equality (sqrt(x+a)+sqrt(b - x)=sqrt(a+b))",
32.430 "solveFor x","solutions L"];
32.431 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
32.432 +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
32.433
32.434 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
32.435 (* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"])*)
32.436 @@ -1657,7 +1657,7 @@
32.437 "Schalk II s.68 Bsp 62b (sqrt((x+a)^^^2+(x - 2*b)^^^2)=a+2*b)";
32.438 val fmz = ["equality (sqrt((x+a)^^^2+(x - 2*b)^^^2)=a+2*b)",
32.439 "solveFor x","solutions L"];
32.440 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
32.441 +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
32.442 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
32.443 (*val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"]) *)
32.444 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.445 @@ -1718,7 +1718,7 @@
32.446 (*EO-7*)
32.447 val fmz = ["equality ((2*x+1)*x^^^2 = 0)",
32.448 "solveFor x","solutions L"];
32.449 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
32.450 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
32.451 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
32.452 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.453 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32.454 @@ -1769,7 +1769,7 @@
32.455 (*EO-9*)
32.456 val fmz = ["equality ((a/2)^^^2 + (b/2)^^^2 = r^^^2)",
32.457 "solveFor a","solutions L"];
32.458 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
32.459 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
32.460 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
32.461 (* Model_Problem ["normalize","polynomial","univariate","equation"])*)
32.462 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
32.463 @@ -1779,7 +1779,7 @@
32.464 (*val nxt = ("Apply_Method",Apply_Method ["PolyEq","normalize_poly"])*)
32.465 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
32.466 val (p,_,f,nxt,_,pt) = me nxt p c pt;
32.467 -(*val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"])*)
32.468 +(*val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"])*)
32.469 val (p,_,f,nxt,_,pt) = me nxt p c pt;
32.470 val (p,_,f,nxt,_,pt) = me nxt p c pt;
32.471 (*val nxt =Model_Problem ["sq_only","degree_2","polynomial","univariate","equation"])*)
32.472 @@ -1815,7 +1815,7 @@
32.473 (*EO-10*)
32.474 val fmz = ["equality (2*sqrt(r^^^2 - (u/2)^^^2) - u^^^2/(2*sqrt(r^^^2 - (u/2)^^^2))= 0)",
32.475 "solveFor u","solutions L"];
32.476 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
32.477 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
32.478
32.479 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
32.480 (* Model_Problem ["normalize","root'","univariate","equation"])*)
32.481 @@ -1825,7 +1825,7 @@
32.482 val (p,_,f,nxt,_,pt) = me nxt p c pt;
32.483 (*val nxt = Apply_Method ["RootEq","norm_sq_root_equation"]) *)
32.484 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
32.485 -(*val nxt = Subproblem ("RootEq.thy",["univariate","equation"]))*)
32.486 +(*val nxt = Subproblem ("RootEq",["univariate","equation"]))*)
32.487 val (p,_,f,nxt,_,pt) = me nxt p c pt;
32.488 (*val nxt = Model_Problem ["sq","root'","univariate","equation"]) *)
32.489 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
32.490 @@ -1836,7 +1836,7 @@
32.491 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
32.492 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
32.493 val (p,_,f,nxt,_,pt) = me nxt p c pt;
32.494 -(*val nxt = Subproblem ("RootEq.thy",["univariate","equation"]))*)
32.495 +(*val nxt = Subproblem ("RootEq",["univariate","equation"]))*)
32.496 val (p,_,f,nxt,_,pt) = me nxt p c pt;
32.497 (*val nxt = Model_Problem ["rational","univariate","equation"]) *)
32.498 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
32.499 @@ -1846,7 +1846,7 @@
32.500 (*val nxt = Apply_Method ["RootEq","solve_rat_equation"]) *)
32.501 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
32.502 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
32.503 -(*val nxt = Subproblem ("RootEq.thy",["univariate","equation"]))*)
32.504 +(*val nxt = Subproblem ("RootEq",["univariate","equation"]))*)
32.505 val (p,_,f,nxt,_,pt) = me nxt p c pt;
32.506 (*val nxt = Model_Problem ["normalize","polynomial","univariate","equation"]) *)
32.507 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
32.508 @@ -1856,7 +1856,7 @@
32.509 (*val nxt = Apply_Method ["PolyEq","normalize_poly"]) *)
32.510 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
32.511 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
32.512 -(*val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
32.513 +(*val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)
32.514 if f = Form'
32.515 (FormKF
32.516 (~1,
33.1 --- a/test/Tools/isac/Knowledge/rooteq.sml Wed Sep 08 16:45:27 2010 +0200
33.2 +++ b/test/Tools/isac/Knowledge/rooteq.sml Wed Sep 08 16:47:22 2010 +0200
33.3 @@ -88,7 +88,7 @@
33.4 (*---------rooteq---- 23.8.02 ---------------------*)
33.5 "---------(1/sqrt(x)=5)---------------------";
33.6 val fmz = ["equality (1/sqrt(x)=5)","solveFor x","solutions L"];
33.7 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
33.8 +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
33.9
33.10 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
33.11 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.12 @@ -97,14 +97,14 @@
33.13 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.14 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.15 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.16 -(*"1 / x = 25" -> Subproblem ("RootEq.thy", ["univariate", ...]) *)
33.17 +(*"1 / x = 25" -> Subproblem ("RootEq", ["univariate", ...]) *)
33.18 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.19 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.20 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.21 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.22 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.23 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.24 -(*"1 = 25 * x" -> Subproblem ("RatEq.thy", ["univariate", ...])*)
33.25 +(*"1 = 25 * x" -> Subproblem ("RatEq", ["univariate", ...])*)
33.26 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.27 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.28 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.29 @@ -113,7 +113,7 @@
33.30 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.31 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "1 + -25 * x = 0")) then ()
33.32 else raise error "rooteq.sml: diff.behav.poly in (1/sqrt(x)=5)";
33.33 -(*-> Subproblem ("PolyEq.thy", ["polynomial", ...])*)
33.34 +(*-> Subproblem ("PolyEq", ["polynomial", ...])*)
33.35 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.36 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.37 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.38 @@ -137,7 +137,7 @@
33.39
33.40 "---------(sqrt(x+1)=5)---------------------";
33.41 val fmz = ["equality (sqrt(x+1)=5)","solveFor x","solutions L"];
33.42 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
33.43 +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
33.44 (*val p = e_pos';
33.45 val c = [];
33.46 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
33.47 @@ -149,7 +149,7 @@
33.48 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.49 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.50 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.51 -(*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
33.52 +(*-> Subproblem ("RootEq", ["univariate", ...])*)
33.53 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.54 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.55 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.56 @@ -158,7 +158,7 @@
33.57 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.58 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-24 + x = 0")) then ()
33.59 else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)=5";
33.60 -(*-> Subproblem ("PolyEq.thy", ["polynomial", ...])*)
33.61 +(*-> Subproblem ("PolyEq", ["polynomial", ...])*)
33.62 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.63 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.64 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.65 @@ -173,7 +173,7 @@
33.66
33.67 "-------------(4*sqrt(4*x+2)=3*sqrt(2*x+24))-----------------";
33.68 val fmz = ["equality (4*sqrt(4*x+2)=3*sqrt(2*x+24))","solveFor x","solutions L"];
33.69 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
33.70 +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
33.71
33.72 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
33.73 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.74 @@ -207,7 +207,7 @@
33.75
33.76 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))----------------";
33.77 val fmz = ["equality (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))","solveFor x","solutions L"];
33.78 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
33.79 +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
33.80
33.81 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
33.82 (*val nxt = Model_Problem ["sq","root'","univariate","equation"]) *)
33.83 @@ -219,7 +219,7 @@
33.84 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.85 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.86 (*"13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"))
33.87 -val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*)
33.88 +val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"]))*)
33.89 val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.90 (*val nxt = Model_Problem ["sq","root'","univariate","equation"]) *)
33.91 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.92 @@ -230,7 +230,7 @@
33.93 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.94 val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.95 (*"144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"))
33.96 -val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*)
33.97 +val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"]))*)
33.98 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.99 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.100 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.101 @@ -239,7 +239,7 @@
33.102 val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.103 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
33.104 else raise error "rooteq.sml: diff.behav.poly in (sqrt(x+1)+sqrt(4*x+4)=sqr..";
33.105 -(*-> Subproblem ("PolyEq.thy", ["degree_0", ...])*)
33.106 +(*-> Subproblem ("PolyEq", ["degree_0", ...])*)
33.107 val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.108 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.109 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.110 @@ -260,7 +260,7 @@
33.111 val fmz =
33.112 ["equality (13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x)",
33.113 "solveFor x","solutions L"];
33.114 -val (dI',pI',mI') = ("RootEq.thy",["sq","root'","univariate","equation"],
33.115 +val (dI',pI',mI') = ("RootEq",["sq","root'","univariate","equation"],
33.116 ["RootEq","solve_sq_root_equation"]);
33.117 (*val p = e_pos'; val c = [];
33.118 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
33.119 @@ -274,7 +274,7 @@
33.120 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.121 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.122 (*"144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"))
33.123 -val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"])) *)
33.124 +val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"])) *)
33.125 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.126 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.127 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.128 @@ -283,7 +283,7 @@
33.129 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.130 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.131 (*val p = ([6,2],Res) val f = Form' (FormKF (~1,EdUndef,2,Nundef,"0 = 0"))
33.132 -val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
33.133 +val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)
33.134 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
33.135 else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
33.136 val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.137 @@ -311,7 +311,7 @@
33.138
33.139 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- OKversion----";
33.140 val fmz = ["equality (sqrt(x) = 1)","solveFor x","solutions L"];
33.141 -val (dI',pI',mI') = ("RootEq.thy",["sq","root'","univariate","equation"],
33.142 +val (dI',pI',mI') = ("RootEq",["sq","root'","univariate","equation"],
33.143 ["RootEq","solve_sq_root_equation"]);
33.144 (*val p = e_pos'; val c = [];
33.145 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
33.146 @@ -326,7 +326,7 @@
33.147 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.148 val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.149 (* val p = ([2],Res) val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = 1"))
33.150 -val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*)
33.151 +val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"]))*)
33.152 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.153 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.154 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.155 @@ -335,7 +335,7 @@
33.156 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.157 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.158 (*val p = ([3,2],Res)val f = Form' (FormKF (~1,EdUndef,2,Nundef,"-1 + x = 0"))
33.159 -val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
33.160 +val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)
33.161 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-1 + x = 0")) then ()
33.162 else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
33.163 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.164 @@ -372,7 +372,7 @@
33.165 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- SHORTEST.1.----\
33.166 \ with same error";
33.167 val fmz = ["equality (sqrt x = sqrt x)","solveFor x","solutions L"];
33.168 -val (dI',pI',mI') = ("RootEq.thy",["sq","root'","univariate","equation"],
33.169 +val (dI',pI',mI') = ("RootEq",["sq","root'","univariate","equation"],
33.170 ["RootEq","solve_sq_root_equation"]);
33.171 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
33.172 val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.173 @@ -383,7 +383,7 @@
33.174 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.175 val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.176 (*val p = ([1],Res) val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = x"))
33.177 -val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*)
33.178 +val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"]))*)
33.179 val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.180 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.181 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.182 @@ -392,7 +392,7 @@
33.183 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.184 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.185 (*val p = ([2,2],Res) val f = Form' (FormKF (~1,EdUndef,2,Nundef,"0 = 0"))
33.186 -val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
33.187 +val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)
33.188 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
33.189 else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
33.190 val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.191 @@ -420,7 +420,7 @@
33.192
33.193 "--------------(3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))----------------";
33.194 val fmz = ["equality (3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))","solveFor x","solutions L"];
33.195 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
33.196 +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
33.197
33.198 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
33.199 val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.200 @@ -431,7 +431,7 @@
33.201 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.202 val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.203 (* "6 + x = 60 + 13 * x + -6 * sqrt ((3 + x) * (33 + 4 * x))")) : mout
33.204 -val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*)
33.205 +val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"]))*)
33.206 val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.207 (*val nxt = Model_Problem ["sq","root'","univariate","equation"]) *)
33.208 val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.209 @@ -442,7 +442,7 @@
33.210 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.211 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.212 (*"2916 + x ^^^ 2 + 1296 * x + 143 * x ^^^ 2 = 3564 + 1620 * x + 144 * x ^^^ 2"))
33.213 -val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*)
33.214 +val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"]))*)
33.215 val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.216 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.217 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.218 @@ -451,7 +451,7 @@
33.219 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.220 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-648 + -324 * x = 0")) then ()
33.221 else raise error "rooteq.sml: diff.behav.poly in 3*sqrt(x+3)+sqrt(x+6)=sqrt..";
33.222 -(*-> Subproblem ("PolyEq.thy", ["degree_1", ...])*)
33.223 +(*-> Subproblem ("PolyEq", ["degree_1", ...])*)
33.224 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.225 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
33.226 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml Wed Sep 08 16:45:27 2010 +0200
34.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Wed Sep 08 16:47:22 2010 +0200
34.3 @@ -50,7 +50,7 @@
34.4
34.5 "--------------------- test thm rootrat_equation_left_1 ---------------------";
34.6 val fmz = ["equality ( -2 + 1/(1 - sqrt(x))= 0)", "solveFor x","solutions L"];
34.7 -val (dI',pI',mI') = ("RootRatEq.thy",["univariate","equation"],["no_met"]);
34.8 +val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
34.9
34.10 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
34.11 val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.12 @@ -59,21 +59,21 @@
34.13 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.14 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.15 val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.16 -(*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
34.17 +(*-> Subproblem ("RootEq", ["univariate", ...])*)
34.18 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.19 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.20 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.21 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.22 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.23 val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.24 -(*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
34.25 +(*-> Subproblem ("RootEq", ["univariate", ...])*)
34.26 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.27 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.28 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.29 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.30 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.31 val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.32 -(*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
34.33 +(*-> Subproblem ("RootEq", ["univariate", ...])*)
34.34 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.35 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.36 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.37 @@ -82,7 +82,7 @@
34.38 val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.39 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "1 + -4 * x = 0")) then ()
34.40 else raise error "rootrateq.sml: diff.behav. in rootrat_equation_left_1";
34.41 -(*-> Subproblem ("RootEq.thy", ["polynomial", ...])*)
34.42 +(*-> Subproblem ("RootEq", ["polynomial", ...])*)
34.43 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.44 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.45 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.46 @@ -98,7 +98,7 @@
34.47
34.48 "--------------------- test thm rootrat_equation_left_2 ---------------------";
34.49 val fmz = ["equality (3/(1+sqrt(x))= 1)", "solveFor x","solutions L"];
34.50 -val (dI',pI',mI') = ("RootRatEq.thy",["univariate","equation"],["no_met"]);
34.51 +val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
34.52
34.53 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
34.54 val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.55 @@ -106,21 +106,21 @@
34.56 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.57 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.58 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.59 -(*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
34.60 +(*-> Subproblem ("RootEq", ["univariate", ...])*)
34.61 val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.62 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.63 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.64 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.65 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.66 val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.67 -(*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
34.68 +(*-> Subproblem ("RootEq", ["univariate", ...])*)
34.69 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.70 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.71 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.72 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.73 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.74 val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.75 -(*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
34.76 +(*-> Subproblem ("RootEq", ["univariate", ...])*)
34.77 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.78 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.79 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.80 @@ -129,7 +129,7 @@
34.81 val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.82 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "4 + -1 * x = 0")) then ()
34.83 else raise error "rootrateq.sml: diff.behav. in rootrat_equation_left_2";
34.84 -(*-> Subproblem ("PolyEq.thy", ["polynomial", ...])*)
34.85 +(*-> Subproblem ("PolyEq", ["polynomial", ...])*)
34.86 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.87 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.88 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.89 @@ -145,7 +145,7 @@
34.90
34.91 "--------------------- test thm rootrat_equation_right_1 ---------------";
34.92 val fmz = ["equality ( 0= -2 + 1/(1 - sqrt(x)))", "solveFor x","solutions L"];
34.93 -val (dI',pI',mI') = ("RootRatEq.thy",["univariate","equation"],["no_met"]);
34.94 +val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
34.95
34.96 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
34.97 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.98 @@ -188,7 +188,7 @@
34.99
34.100 "--------------------- test thm rootrat_equation_right_2 --------------------";
34.101 val fmz = ["equality (1 = 3/(1+sqrt(x)))", "solveFor x","solutions L"];
34.102 -val (dI',pI',mI') = ("RootRatEq.thy",["univariate","equation"],["no_met"]);
34.103 +val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
34.104
34.105 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
34.106 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
35.1 --- a/test/Tools/isac/Knowledge/simplify.sml Wed Sep 08 16:45:27 2010 +0200
35.2 +++ b/test/Tools/isac/Knowledge/simplify.sml Wed Sep 08 16:47:22 2010 +0200
35.3 @@ -41,7 +41,7 @@
35.4 "----------- append inform with final result ---------------------";
35.5 states:=[];
35.6 CalcTree [(["TERM ((14 * x * y) / ( x * y ))", "normalform N"],
35.7 - ("Rational.thy",["rational","simplification"],
35.8 + ("Rational",["rational","simplification"],
35.9 ["simplification","of_rationals"]))];
35.10 Iterator 1;
35.11 moveActiveRoot 1;
36.1 --- a/test/Tools/isac/Knowledge/system.sml Wed Sep 08 16:45:27 2010 +0200
36.2 +++ b/test/Tools/isac/Knowledge/system.sml Wed Sep 08 16:47:22 2010 +0200
36.3 @@ -47,14 +47,14 @@
36.4 val fmz = ["equalities [0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2, 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2]",
36.5 "solveForVars [c, c_2]", "solution ss___"];
36.6 val (dI',pI',mI') =
36.7 - ("Biegelinie.thy",["normalize","2x2","linear","system"],
36.8 + ("Biegelinie",["normalize","2x2","linear","system"],
36.9 ["EqSystem","normalize","2x2"]);
36.10 val p = e_pos'; val c = [];
36.11 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
36.12 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
36.13 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
36.14 val (p,_,f,nxt,_,pt) = me nxt p c pt;
36.15 -case nxt of (_, Specify_Theory "Biegelinie.thy") => ()
36.16 +case nxt of (_, Specify_Theory "Biegelinie") => ()
36.17 | _ => raise error "system.sml diff.behav.in me --1";
36.18 val (p,_,f,nxt,_,pt) = me nxt p c pt;
36.19 val (p,_,f,nxt,_,pt) = me nxt p c pt;
36.20 @@ -67,14 +67,14 @@
36.21 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
36.22 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
36.23
36.24 -case nxt of (_, Subproblem ("Biegelinie.thy", ["triangular", "2x2",
36.25 +case nxt of (_, Subproblem ("Biegelinie", ["triangular", "2x2",
36.26 "linear", "system"])) => ()
36.27 | _ => raise error "system.sml diff.behav.in me --3";
36.28 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
36.29 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
36.30 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
36.31 val (p,_,f,nxt,_,pt) = me nxt p c pt;
36.32 -case nxt of (_, Specify_Theory "Biegelinie.thy") => ()
36.33 +case nxt of (_, Specify_Theory "Biegelinie") => ()
36.34 | _ => raise error "system.sml diff.behav.in me --1";
36.35 val (p,_,f,nxt,_,pt) = me nxt p c pt;
36.36 val (p,_,f,nxt,_,pt) = me nxt p c pt;
37.1 --- a/test/Tools/isac/Knowledge/termorder.sml Wed Sep 08 16:45:27 2010 +0200
37.2 +++ b/test/Tools/isac/Knowledge/termorder.sml Wed Sep 08 16:47:22 2010 +0200
37.3 @@ -72,7 +72,7 @@
37.4 else raise error "termorder.sml diff.behav ord_make_polynomial_in #14";
37.5
37.6 val SOME (t',_) =
37.7 - rewrite_set_inst "Isac.thy"false [("bdv","x")] "make_polynomial_in" ppp';
37.8 + rewrite_set_inst "Isac"false [("bdv","x")] "make_polynomial_in" ppp';
37.9 (*MG 2003...
37.10 "(-6) + (-5 * x + (-15) * x ^^^ 2)";*)
37.11 if t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()