1.1 --- a/src/Tools/isac/Interpret/calchead.sml Thu Sep 23 08:43:36 2010 +0200
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Thu Sep 23 08:54:26 2010 +0200
1.3 @@ -928,7 +928,6 @@
1.4 of a SubProblem ? see ME/ptyps.sml 'type met '.*)
1.5 fun is_copy_named_idstr str =
1.6 case (rev o explode) str of
1.7 - (*"_":: _ ::"_"::_ => true*)
1.8 "'":: _ ::"'"::_ => (tracing ((strs2str o (rev o explode))
1.9 "is_copy_named_idstr: " ^ str ^ " T"); true)
1.10 | _ => (tracing ((strs2str o (rev o explode))
1.11 @@ -939,7 +938,6 @@
1.12 fun is_copy_named_generating_idstr str =
1.13 if is_copy_named_idstr str
1.14 then case (rev o explode) str of
1.15 - (*"_"::"_"::"_"::_ => false*)
1.16 "'"::"'"::"'"::_ => false
1.17 | _ => true
1.18 else false;
1.19 @@ -1007,7 +1005,8 @@
1.20
1.21 (* generate a new variable "x_i" name from a related given one "x"
1.22 by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
1.23 - e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i) *)
1.24 + e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
1.25 + but leave is_copy_named_generating as is, e.t. ss''' *)
1.26 fun cpy_nam (pbt:pat list) (oris:preori list) (p as (field,(dsc,t)):pat) =
1.27 (if is_copy_named_generating p
1.28 then (*WN051014 kept strange old code ...*)
2.1 --- a/src/Tools/isac/Knowledge/Equation.thy Thu Sep 23 08:43:36 2010 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Thu Sep 23 08:54:26 2010 +0200
2.3 @@ -44,7 +44,7 @@
2.4 (["equation"],
2.5 [("#Given" ,["equality e_e","solveFor v_v"]),
2.6 ("#Where" ,["matches (?a = ?b) e_e"]),
2.7 - ("#Find" ,["solutions v'i'"])
2.8 + ("#Find" ,["solutions v_v'i'"])
2.9 ],
2.10 append_rls "equation_prls" e_rls
2.11 [Calc ("Tools.matches",eval_matches "")],
2.12 @@ -56,7 +56,7 @@
2.13 (["univariate","equation"],
2.14 [("#Given" ,["equality e_e","solveFor v_v"]),
2.15 ("#Where" ,["matches (?a = ?b) e_e"]),
2.16 - ("#Find" ,["solutions v'i'"])
2.17 + ("#Find" ,["solutions v_v'i'"])
2.18 ],
2.19 univariate_equation_prls,SOME "solve (e_e::bool, v_v)",[]));
2.20
3.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Thu Sep 23 08:43:36 2010 +0200
3.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Thu Sep 23 08:54:26 2010 +0200
3.3 @@ -134,7 +134,7 @@
3.4 "Not( (rhs e_e) is_polyrat_in v_v)",
3.5 "((lhs e_e) has_degree_in v_v)=1",
3.6 "((rhs e_e) has_degree_in v_v)=1"]),
3.7 - ("#Find" ,["solutions v'i'"])
3.8 + ("#Find" ,["solutions v_v'i'"])
3.9 ],
3.10 LinEq_prls, SOME "solve (e_e::bool, v_v)",
3.11 [["LinEq","solve_lineq_equation"]]));
3.12 @@ -155,7 +155,7 @@
3.13 [("#Given", ["equality e_e", "solveFor v_v"]),
3.14 ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)",
3.15 "((lhs e_e) has_degree_in v_v) = 1"]),
3.16 - ("#Find", ["solutions v'i'"])
3.17 + ("#Find", ["solutions v_v'i'"])
3.18 ],
3.19 {rew_ord'="termlessI", rls'=LinEq_erls, srls=e_rls, prls=LinEq_prls,
3.20 calc=[], crls=LinEq_crls, nrls=norm_Poly},
4.1 --- a/src/Tools/isac/Knowledge/LogExp.thy Thu Sep 23 08:43:36 2010 +0200
4.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy Thu Sep 23 08:54:26 2010 +0200
4.3 @@ -33,7 +33,7 @@
4.4 (["logarithmic","univariate","equation"],
4.5 [("#Given",["equality e_e","solveFor v_v"]),
4.6 ("#Where",["matches ((?a log ?v_v) = ?b) e_e"]),
4.7 - ("#Find" ,["solutions v'i'"]),
4.8 + ("#Find" ,["solutions v_v'i'"]),
4.9 ("#With" ,["||(lhs (Subst (v'i', v_v) e_e) - " ^
4.10 " (rhs (Subst (v'i', v_v) e_e) || < eps)"])
4.11 ],
4.12 @@ -47,7 +47,7 @@
4.13 (["Equation","solve_log"],
4.14 [("#Given" ,["equality e_e","solveFor v_v"]),
4.15 ("#Where" ,["matches ((?a log ?v_v) = ?b) e_e"]),
4.16 - ("#Find" ,["solutions v'i'"])
4.17 + ("#Find" ,["solutions v_v'i'"])
4.18 ],
4.19 {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
4.20 calc=[],crls=PolyEq_crls, nrls=norm_Rational},
5.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Thu Sep 23 08:43:36 2010 +0200
5.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Thu Sep 23 08:54:26 2010 +0200
5.3 @@ -849,7 +849,7 @@
5.4 ("#Where" ,["~((e_e::bool) is_ratequation_in (v_v::real))",
5.5 "~((lhs e_e) is_rootTerm_in (v_v::real))",
5.6 "~((rhs e_e) is_rootTerm_in (v_v::real))"]),
5.7 - ("#Find" ,["solutions v'i'"])
5.8 + ("#Find" ,["solutions v_v'i'"])
5.9 ],
5.10 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
5.11 []));
5.12 @@ -862,7 +862,7 @@
5.13 "(lhs e_e) is_poly_in v_v",
5.14 "((lhs e_e) has_degree_in v_v ) = 0"
5.15 ]),
5.16 - ("#Find" ,["solutions v'i'"])
5.17 + ("#Find" ,["solutions v_v'i'"])
5.18 ],
5.19 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
5.20 [["PolyEq","solve_d0_polyeq_equation"]]));
5.21 @@ -876,7 +876,7 @@
5.22 "(lhs e_e) is_poly_in v_v",
5.23 "((lhs e_e) has_degree_in v_v ) = 1"
5.24 ]),
5.25 - ("#Find" ,["solutions v'i'"])
5.26 + ("#Find" ,["solutions v_v'i'"])
5.27 ],
5.28 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
5.29 [["PolyEq","solve_d1_polyeq_equation"]]));
5.30 @@ -890,7 +890,7 @@
5.31 ("#Where" ,["matches (?a = 0) e_e",
5.32 "(lhs e_e) is_poly_in v_v ",
5.33 "((lhs e_e) has_degree_in v_v ) = 2"]),
5.34 - ("#Find" ,["solutions v'i'"])
5.35 + ("#Find" ,["solutions v_v'i'"])
5.36 ],
5.37 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
5.38 [["PolyEq","solve_d2_polyeq_equation"]]));
5.39 @@ -911,7 +911,7 @@
5.40 "Not (matches ( ?b*?v_ + ?v_^^^2 = 0) e_e) &" ^
5.41 "Not (matches ( ?v_ + ?c*?v_^^^2 = 0) e_e) &" ^
5.42 "Not (matches ( ?b*?v_ + ?c*?v_^^^2 = 0) e_e)"]),
5.43 - ("#Find" ,["solutions v'i'"])
5.44 + ("#Find" ,["solutions v_v'i'"])
5.45 ],
5.46 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
5.47 [["PolyEq","solve_d2_polyeq_sqonly_equation"]]));
5.48 @@ -926,7 +926,7 @@
5.49 "matches (?a*?v_ + ?b*?v_^^^2 = 0) e_e | " ^
5.50 "matches ( ?v_^^^2 = 0) e_e | " ^
5.51 "matches ( ?b*?v_^^^2 = 0) e_e "]),
5.52 - ("#Find" ,["solutions v'i'"])
5.53 + ("#Find" ,["solutions v_v'i'"])
5.54 ],
5.55 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
5.56 [["PolyEq","solve_d2_polyeq_bdvonly_equation"]]));
5.57 @@ -937,7 +937,7 @@
5.58 [("#Given" ,["equality e_e","solveFor v_v"]),
5.59 ("#Where" ,["matches (?a + 1*?v_^^^2 = 0) e_e | " ^
5.60 "matches (?a + ?v_^^^2 = 0) e_e"]),
5.61 - ("#Find" ,["solutions v'i'"])
5.62 + ("#Find" ,["solutions v_v'i'"])
5.63 ],
5.64 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
5.65 [["PolyEq","solve_d2_polyeq_pq_equation"]]));
5.66 @@ -948,7 +948,7 @@
5.67 [("#Given" ,["equality e_e","solveFor v_v"]),
5.68 ("#Where" ,["matches (?a + ?v_^^^2 = 0) e_e | " ^
5.69 "matches (?a + ?b*?v_^^^2 = 0) e_e"]),
5.70 - ("#Find" ,["solutions v'i'"])
5.71 + ("#Find" ,["solutions v_v'i'"])
5.72 ],
5.73 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
5.74 [["PolyEq","solve_d2_polyeq_abc_equation"]]));
5.75 @@ -962,7 +962,7 @@
5.76 ("#Where" ,["matches (?a = 0) e_e",
5.77 "(lhs e_e) is_poly_in v_v ",
5.78 "((lhs e_e) has_degree_in v_v) = 3"]),
5.79 - ("#Find" ,["solutions v'i'"])
5.80 + ("#Find" ,["solutions v_v'i'"])
5.81 ],
5.82 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
5.83 [["PolyEq","solve_d3_polyeq_equation"]]));
5.84 @@ -975,7 +975,7 @@
5.85 ("#Where" ,["matches (?a = 0) e_e",
5.86 "(lhs e_e) is_poly_in v_v ",
5.87 "((lhs e_e) has_degree_in v_v) = 4"]),
5.88 - ("#Find" ,["solutions v'i'"])
5.89 + ("#Find" ,["solutions v_v'i'"])
5.90 ],
5.91 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
5.92 [(*["PolyEq","solve_d4_polyeq_equation"]*)]));
5.93 @@ -987,7 +987,7 @@
5.94 [("#Given" ,["equality e_e","solveFor v_v"]),
5.95 ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) |" ^
5.96 "(Not(((lhs e_e) is_poly_in v_v)))"]),
5.97 - ("#Find" ,["solutions v'i'"])
5.98 + ("#Find" ,["solutions v_v'i'"])
5.99 ],
5.100 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
5.101 [["PolyEq","normalize_poly"]]));
5.102 @@ -998,7 +998,7 @@
5.103 [("#Given" ,["equality e_e","solveFor v_v"]),
5.104 ("#Where" ,["matches (?a = 0) e_e",
5.105 "(lhs e_e) is_expanded_in v_v "]),
5.106 - ("#Find" ,["solutions v'i'"])
5.107 + ("#Find" ,["solutions v_v'i'"])
5.108 ],
5.109 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
5.110 []));
5.111 @@ -1009,7 +1009,7 @@
5.112 (["degree_2","expanded","univariate","equation"],
5.113 [("#Given" ,["equality e_e","solveFor v_v"]),
5.114 ("#Where" ,["((lhs e_e) has_degree_in v_v) = 2"]),
5.115 - ("#Find" ,["solutions v'i'"])
5.116 + ("#Find" ,["solutions v_v'i'"])
5.117 ],
5.118 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
5.119 [["PolyEq","complete_square"]]));
5.120 @@ -1043,7 +1043,7 @@
5.121 [("#Given" ,["equality e_e","solveFor v_v"]),
5.122 ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) |" ^
5.123 "(Not(((lhs e_e) is_poly_in v_v)))"]),
5.124 - ("#Find" ,["solutions v'i'"])
5.125 + ("#Find" ,["solutions v_v'i'"])
5.126 ],
5.127 {rew_ord'="termlessI",
5.128 rls'=PolyEq_erls,
5.129 @@ -1070,7 +1070,7 @@
5.130 [("#Given" ,["equality e_e","solveFor v_v"]),
5.131 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
5.132 "((lhs e_e) has_degree_in v_v) = 0"]),
5.133 - ("#Find" ,["solutions v'i'"])
5.134 + ("#Find" ,["solutions v_v'i'"])
5.135 ],
5.136 {rew_ord'="termlessI",
5.137 rls'=PolyEq_erls,
5.138 @@ -1091,7 +1091,7 @@
5.139 [("#Given" ,["equality e_e","solveFor v_v"]),
5.140 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
5.141 "((lhs e_e) has_degree_in v_v) = 1"]),
5.142 - ("#Find" ,["solutions v'i'"])
5.143 + ("#Find" ,["solutions v_v'i'"])
5.144 ],
5.145 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
5.146 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
5.147 @@ -1112,7 +1112,7 @@
5.148 [("#Given" ,["equality e_e","solveFor v_v"]),
5.149 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
5.150 "((lhs e_e) has_degree_in v_v) = 2"]),
5.151 - ("#Find" ,["solutions v'i'"])
5.152 + ("#Find" ,["solutions v_v'i'"])
5.153 ],
5.154 {rew_ord'="termlessI",
5.155 rls'=PolyEq_erls,
5.156 @@ -1139,7 +1139,7 @@
5.157 [("#Given" ,["equality e_e","solveFor v_v"]),
5.158 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
5.159 "((lhs e_e) has_degree_in v_v) = 2"]),
5.160 - ("#Find" ,["solutions v'i'"])
5.161 + ("#Find" ,["solutions v_v'i'"])
5.162 ],
5.163 {rew_ord'="termlessI",
5.164 rls'=PolyEq_erls,
5.165 @@ -1166,7 +1166,7 @@
5.166 [("#Given" ,["equality e_e","solveFor v_v"]),
5.167 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
5.168 "((lhs e_e) has_degree_in v_v) = 2"]),
5.169 - ("#Find" ,["solutions v'i'"])
5.170 + ("#Find" ,["solutions v_v'i'"])
5.171 ],
5.172 {rew_ord'="termlessI",
5.173 rls'=PolyEq_erls,
5.174 @@ -1190,7 +1190,7 @@
5.175 [("#Given" ,["equality e_e","solveFor v_v"]),
5.176 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
5.177 "((lhs e_e) has_degree_in v_v) = 2"]),
5.178 - ("#Find" ,["solutions v'i'"])
5.179 + ("#Find" ,["solutions v_v'i'"])
5.180 ],
5.181 {rew_ord'="termlessI",
5.182 rls'=PolyEq_erls,
5.183 @@ -1214,7 +1214,7 @@
5.184 [("#Given" ,["equality e_e","solveFor v_v"]),
5.185 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
5.186 "((lhs e_e) has_degree_in v_v) = 2"]),
5.187 - ("#Find" ,["solutions v'i'"])
5.188 + ("#Find" ,["solutions v_v'i'"])
5.189 ],
5.190 {rew_ord'="termlessI",
5.191 rls'=PolyEq_erls,
5.192 @@ -1238,7 +1238,7 @@
5.193 [("#Given" ,["equality e_e","solveFor v_v"]),
5.194 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
5.195 "((lhs e_e) has_degree_in v_v) = 3"]),
5.196 - ("#Find" ,["solutions v'i'"])
5.197 + ("#Find" ,["solutions v_v'i'"])
5.198 ],
5.199 {rew_ord'="termlessI",
5.200 rls'=PolyEq_erls,
5.201 @@ -1271,7 +1271,7 @@
5.202 [("#Given" ,["equality e_e","solveFor v_v"]),
5.203 ("#Where" ,["matches (?a = 0) e_e",
5.204 "((lhs e_e) has_degree_in v_v) = 2"]),
5.205 - ("#Find" ,["solutions v'i'"])
5.206 + ("#Find" ,["solutions v_v'i'"])
5.207 ],
5.208 {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
5.209 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
6.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Thu Sep 23 08:43:36 2010 +0200
6.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Thu Sep 23 08:54:26 2010 +0200
6.3 @@ -175,7 +175,7 @@
6.4 (["rational","univariate","equation"],
6.5 [("#Given" ,["equality e_e","solveFor v_v"]),
6.6 ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]),
6.7 - ("#Find" ,["solutions v'i'"])
6.8 + ("#Find" ,["solutions v_v'i'"])
6.9 ],
6.10
6.11 RatEq_prls, SOME "solve (e_e::bool, v_v)",
6.12 @@ -199,7 +199,7 @@
6.13 (["RatEq","solve_rat_equation"],
6.14 [("#Given" ,["equality e_e","solveFor v_v"]),
6.15 ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]),
6.16 - ("#Find" ,["solutions v'i'"])
6.17 + ("#Find" ,["solutions v_v'i'"])
6.18 ],
6.19 {rew_ord'="termlessI",
6.20 rls'=rateq_erls,
7.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Thu Sep 23 08:43:36 2010 +0200
7.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Thu Sep 23 08:54:26 2010 +0200
7.3 @@ -482,7 +482,7 @@
7.4 [("#Given" ,["equality e_e","solveFor v_v"]),
7.5 ("#Where" ,["(lhs e_e) is_rootTerm_in (v_v::real) | " ^
7.6 "(rhs e_e) is_rootTerm_in (v_v::real)"]),
7.7 - ("#Find" ,["solutions v'i'"])
7.8 + ("#Find" ,["solutions v_v'i'"])
7.9 ],
7.10 RootEq_prls, SOME "solve (e_e::bool, v_v)",
7.11 []));
7.12 @@ -495,7 +495,7 @@
7.13 " ((lhs e_e) is_normSqrtTerm_in (v_v::real)) ) |" ^
7.14 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
7.15 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)) )"]),
7.16 - ("#Find" ,["solutions v'i'"])
7.17 + ("#Find" ,["solutions v_v'i'"])
7.18 ],
7.19 RootEq_prls, SOME "solve (e_e::bool, v_v)",
7.20 [["RootEq","solve_sq_root_equation"]]));
7.21 @@ -508,7 +508,7 @@
7.22 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^
7.23 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
7.24 " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
7.25 - ("#Find" ,["solutions v'i'"])
7.26 + ("#Find" ,["solutions v_v'i'"])
7.27 ],
7.28 RootEq_prls, SOME "solve (e_e::bool, v_v)",
7.29 [["RootEq","norm_sq_root_equation"]]));
7.30 @@ -532,7 +532,7 @@
7.31 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^
7.32 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
7.33 " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
7.34 - ("#Find" ,["solutions v'i'"])
7.35 + ("#Find" ,["solutions v_v'i'"])
7.36 ],
7.37 {rew_ord'="termlessI", rls'=RootEq_erls, srls=e_rls, prls=RootEq_prls,
7.38 calc=[], crls=RootEq_crls, nrls=norm_Poly},
7.39 @@ -558,7 +558,7 @@
7.40 " ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |" ^
7.41 "(((rhs e_e) is_sqrtTerm_in (v_v::real)) & " ^
7.42 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
7.43 - ("#Find" ,["solutions v'i'"])
7.44 + ("#Find" ,["solutions v_v'i'"])
7.45 ],
7.46 {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls,
7.47 prls = RootEq_prls, calc = [], crls=RootEq_crls, nrls=norm_Poly},
7.48 @@ -586,7 +586,7 @@
7.49 (["RootEq","solve_right_sq_root_equation"],
7.50 [("#Given" ,["equality e_e","solveFor v_v"]),
7.51 ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]),
7.52 - ("#Find" ,["solutions v'i'"])
7.53 + ("#Find" ,["solutions v_v'i'"])
7.54 ],
7.55 {rew_ord' = "termlessI", rls' = RootEq_erls, srls = e_rls,
7.56 prls = RootEq_prls, calc = [], crls = RootEq_crls, nrls = norm_Poly},
7.57 @@ -611,7 +611,7 @@
7.58 (["RootEq","solve_left_sq_root_equation"],
7.59 [("#Given" ,["equality e_e","solveFor v_v"]),
7.60 ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]),
7.61 - ("#Find" ,["solutions v'i'"])
7.62 + ("#Find" ,["solutions v_v'i'"])
7.63 ],
7.64 {rew_ord'="termlessI",
7.65 rls'=RootEq_erls,
8.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Thu Sep 23 08:43:36 2010 +0200
8.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Thu Sep 23 08:54:26 2010 +0200
8.3 @@ -144,7 +144,7 @@
8.4 [("#Given" ,["equality e_e","solveFor v_v"]),
8.5 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) )| " ^
8.6 "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]),
8.7 - ("#Find" ,["solutions v'i'"])
8.8 + ("#Find" ,["solutions v_v'i'"])
8.9 ],
8.10 RootRatEq_prls, SOME "solve (e_e::bool, v_v)",
8.11 [["RootRatEq","elim_rootrat_equation"]]));
8.12 @@ -164,7 +164,7 @@
8.13 [("#Given" ,["equality e_e","solveFor v_v"]),
8.14 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) ) | " ^
8.15 "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]),
8.16 - ("#Find" ,["solutions v'i'"])
8.17 + ("#Find" ,["solutions v_v'i'"])
8.18 ],
8.19 {rew_ord'="termlessI",
8.20 rls'=RooRatEq_erls,
9.1 --- a/src/Tools/isac/Knowledge/Test.thy Thu Sep 23 08:43:36 2010 +0200
9.2 +++ b/src/Tools/isac/Knowledge/Test.thy Thu Sep 23 08:54:26 2010 +0200
9.3 @@ -522,7 +522,7 @@
9.4 (["equation","test"],
9.5 [("#Given" ,["equality e_e","solveFor v_v"]),
9.6 ("#Where" ,["matches (?a = ?b) e_e"]),
9.7 - ("#Find" ,["solutions v'i'"])
9.8 + ("#Find" ,["solutions v_v'i'"])
9.9 ],
9.10 assoc_rls "matches",
9.11 SOME "solve (e_e::bool, v_v)", []));
9.12 @@ -543,7 +543,7 @@
9.13 [("#Given" ,["equality e_e","solveFor v_v"]),
9.14 ("#Where" ,["(matches ( v_v = 0) e_e) | (matches ( ?b*v_v = 0) e_e) |" ^
9.15 "(matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e) "]),
9.16 - ("#Find" ,["solutions v'i'"])
9.17 + ("#Find" ,["solutions v_v'i'"])
9.18 ],
9.19 assoc_rls "matches",
9.20 SOME "solve (e_e::bool, v_v)", [["Test","solve_linear"]]));
9.21 @@ -595,7 +595,7 @@
9.22 (["Test","solve_linear"]:metID,
9.23 [("#Given" ,["equality e_e","solveFor v_v"]),
9.24 ("#Where" ,["matches (?a = ?b) e_e"]),
9.25 - ("#Find" ,["solutions v'i'"])
9.26 + ("#Find" ,["solutions v_v'i'"])
9.27 ],
9.28 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
9.29 prls = assoc_rls "matches", calc = [], crls = tval_rls,
9.30 @@ -783,7 +783,7 @@
9.31 "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^
9.32 "(matches (?a + v_v ^^^2 = 0) e_e) |" ^
9.33 "(matches ( v_v ^^^2 = 0) e_e)"]),
9.34 - ("#Find" ,["solutions v'i'"])
9.35 + ("#Find" ,["solutions v_v'i'"])
9.36 ],
9.37 assoc_rls "matches",
9.38 SOME "solve (e_e::bool, v_v)", [["Test","solve_plain_square"]]));
9.39 @@ -817,7 +817,7 @@
9.40 (["polynomial","univariate","equation","test"],
9.41 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
9.42 ("#Where" ,["False"]),
9.43 - ("#Find" ,["solutions v'i'"])
9.44 + ("#Find" ,["solutions v_v'i'"])
9.45 ],
9.46 e_rls, SOME "solve (e_e::bool, v_v)", []));
9.47
9.48 @@ -825,7 +825,7 @@
9.49 (prep_pbt thy "pbl_test_uni_poly_deg2" [] e_pblID
9.50 (["degree_two","polynomial","univariate","equation","test"],
9.51 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
9.52 - ("#Find" ,["solutions v'i'"])
9.53 + ("#Find" ,["solutions v_v'i'"])
9.54 ],
9.55 e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", []));
9.56
9.57 @@ -833,7 +833,7 @@
9.58 (prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] e_pblID
9.59 (["pq_formula","degree_two","polynomial","univariate","equation","test"],
9.60 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
9.61 - ("#Find" ,["solutions v'i'"])
9.62 + ("#Find" ,["solutions v_v'i'"])
9.63 ],
9.64 e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", []));
9.65
9.66 @@ -841,7 +841,7 @@
9.67 (prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] e_pblID
9.68 (["abc_formula","degree_two","polynomial","univariate","equation","test"],
9.69 [("#Given" ,["equality (a_a * x ^^^2 + b_b * x + c_c = 0)","solveFor v_v"]),
9.70 - ("#Find" ,["solutions v'i'"])
9.71 + ("#Find" ,["solutions v_v'i'"])
9.72 ],
9.73 e_rls, SOME "solve (a_a * x ^^^2 + b_b * x + c_c = 0, v_v)", []));
9.74
9.75 @@ -852,7 +852,7 @@
9.76 (["squareroot","univariate","equation","test"],
9.77 [("#Given" ,["equality e_e","solveFor v_v"]),
9.78 ("#Where" ,["contains_root (e_e::bool)"]),
9.79 - ("#Find" ,["solutions v'i'"])
9.80 + ("#Find" ,["solutions v_v'i'"])
9.81 ],
9.82 append_rls "contains_root" e_rls [Calc ("Test.contains'_root",
9.83 eval_contains_root "#contains_root_")],
9.84 @@ -863,7 +863,7 @@
9.85 (["normalize","univariate","equation","test"],
9.86 [("#Given" ,["equality e_e","solveFor v_v"]),
9.87 ("#Where" ,[]),
9.88 - ("#Find" ,["solutions v'i'"])
9.89 + ("#Find" ,["solutions v_v'i'"])
9.90 ],
9.91 e_rls, SOME "solve (e_e::bool, v_v)", [["Test","norm_univar_equation"]]));
9.92
9.93 @@ -872,7 +872,7 @@
9.94 (["sqroot-test","univariate","equation","test"],
9.95 [("#Given" ,["equality e_e","solveFor v_v"]),
9.96 (*("#Where" ,["contains_root (e_e::bool)"]),*)
9.97 - ("#Find" ,["solutions v'i'"])
9.98 + ("#Find" ,["solutions v_v'i'"])
9.99 ],
9.100 e_rls, SOME "solve (e_e::bool, v_v)", []));
9.101
9.102 @@ -889,7 +889,7 @@
9.103 (["Test","sqrt-equ-test"]:metID,
9.104 [("#Given" ,["equality e_e","solveFor v_v"]),
9.105 ("#Where" ,["contains_root (e_e::bool)"]),
9.106 - ("#Find" ,["solutions v'i'"])
9.107 + ("#Find" ,["solutions v_v'i'"])
9.108 ],
9.109 {rew_ord'="e_rew_ord",rls'=tval_rls,
9.110 srls =append_rls "srls_contains_root" e_rls
9.111 @@ -923,7 +923,7 @@
9.112 (*root-equation ... for test-*.sml until 8.01*)
9.113 (["Test","squ-equ-test2"]:metID,
9.114 [("#Given" ,["equality e_e","solveFor v_v"]),
9.115 - ("#Find" ,["solutions v'i'"])
9.116 + ("#Find" ,["solutions v_v'i'"])
9.117 ],
9.118 {rew_ord'="e_rew_ord",rls'=tval_rls,
9.119 srls = append_rls "srls_contains_root" e_rls
9.120 @@ -957,7 +957,7 @@
9.121 (*tests subproblem fixed linear*)
9.122 (["Test","squ-equ-test-subpbl1"]:metID,
9.123 [("#Given" ,["equality e_e","solveFor v_v"]),
9.124 - ("#Find" ,["solutions v'i'"])
9.125 + ("#Find" ,["solutions v_v'i'"])
9.126 ],
9.127 {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
9.128 crls=tval_rls, nrls=Test_simplify},
9.129 @@ -978,7 +978,7 @@
9.130 (*tests subproblem fixed degree 2*)
9.131 (["Test","squ-equ-test-subpbl2"]:metID,
9.132 [("#Given" ,["equality e_e","solveFor v_v"]),
9.133 - ("#Find" ,["solutions v'i'"])
9.134 + ("#Find" ,["solutions v_v'i'"])
9.135 ],
9.136 {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
9.137 crls=tval_rls, nrls=e_rls(*,
9.138 @@ -998,7 +998,7 @@
9.139 (*root-equation: see foils..., but notTerminating*)
9.140 (["Test","square_equation...notTerminating"]:metID,
9.141 [("#Given" ,["equality e_e","solveFor v_v"]),
9.142 - ("#Find" ,["solutions v'i'"])
9.143 + ("#Find" ,["solutions v_v'i'"])
9.144 ],
9.145 {rew_ord'="e_rew_ord",rls'=tval_rls,
9.146 srls = append_rls "srls_contains_root" e_rls
9.147 @@ -1031,7 +1031,7 @@
9.148 (*root-equation1:*)
9.149 (["Test","square_equation1"]:metID,
9.150 [("#Given" ,["equality e_e","solveFor v_v"]),
9.151 - ("#Find" ,["solutions v'i'"])
9.152 + ("#Find" ,["solutions v_v'i'"])
9.153 ],
9.154 {rew_ord'="e_rew_ord",rls'=tval_rls,
9.155 srls = append_rls "srls_contains_root" e_rls
9.156 @@ -1063,7 +1063,7 @@
9.157 (*root-equation2*)
9.158 (["Test","square_equation2"]:metID,
9.159 [("#Given" ,["equality e_e","solveFor v_v"]),
9.160 - ("#Find" ,["solutions v'i'"])
9.161 + ("#Find" ,["solutions v_v'i'"])
9.162 ],
9.163 {rew_ord'="e_rew_ord",rls'=tval_rls,
9.164 srls = append_rls "srls_contains_root" e_rls
9.165 @@ -1096,7 +1096,7 @@
9.166 (*root-equation*)
9.167 (["Test","square_equation"]:metID,
9.168 [("#Given" ,["equality e_e","solveFor v_v"]),
9.169 - ("#Find" ,["solutions v'i'"])
9.170 + ("#Find" ,["solutions v_v'i'"])
9.171 ],
9.172 {rew_ord'="e_rew_ord",rls'=tval_rls,
9.173 srls = append_rls "srls_contains_root" e_rls
9.174 @@ -1133,7 +1133,7 @@
9.175 "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^
9.176 "(matches (?a + v_v ^^^2 = 0) e_e) |" ^
9.177 "(matches ( v_v ^^^2 = 0) e_e)"]),
9.178 - ("#Find" ,["solutions v'i'"])
9.179 + ("#Find" ,["solutions v_v'i'"])
9.180 ],
9.181 {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=e_rls,
9.182 prls = assoc_rls "matches",
9.183 @@ -1155,7 +1155,7 @@
9.184 (["Test","norm_univar_equation"]:metID,
9.185 [("#Given",["equality e_e","solveFor v_v"]),
9.186 ("#Where" ,[]),
9.187 - ("#Find" ,["solutions v'i'"])
9.188 + ("#Find" ,["solutions v_v'i'"])
9.189 ],
9.190 {rew_ord'="e_rew_ord",rls'=tval_rls,srls = e_rls,prls=e_rls,
9.191 calc=[],
10.1 --- a/test/Tools/isac/Test_Isac.thy Thu Sep 23 08:43:36 2010 +0200
10.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Sep 23 08:54:26 2010 +0200
10.3 @@ -77,9 +77,9 @@
10.4 use"complex.sml";
10.5 use"diff.sml";
10.6 use"diffapp.sml";
10.7 -*)
10.8 +(**)
10.9 use"Knowledge/integrate.sml";
10.10 -(*
10.11 +(**)
10.12 use"equation.sml";
10.13 (*use"inssort.sml"; problems with recdef in Isabelle2002*)
10.14 use"logexp.sml";