1.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Mon Sep 13 18:37:16 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Tue Sep 14 12:12:42 2010 +0200
1.3 @@ -849,7 +849,7 @@
1.4 ("#Where" ,["~((e_e::bool) is_ratequation_in (v_v::real))",
1.5 "~((lhs e_e) is_rootTerm_in (v_v::real))",
1.6 "~((rhs e_e) is_rootTerm_in (v_v::real))"]),
1.7 - ("#Find" ,["solutions v_i"])
1.8 + ("#Find" ,["solutions v_i'''"])
1.9 ],
1.10 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
1.11 []));
1.12 @@ -862,7 +862,7 @@
1.13 "(lhs e_e) is_poly_in v_v",
1.14 "((lhs e_e) has_degree_in v_v ) = 0"
1.15 ]),
1.16 - ("#Find" ,["solutions v_i"])
1.17 + ("#Find" ,["solutions v_i'''"])
1.18 ],
1.19 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
1.20 [["PolyEq","solve_d0_polyeq_equation"]]));
1.21 @@ -876,7 +876,7 @@
1.22 "(lhs e_e) is_poly_in v_v",
1.23 "((lhs e_e) has_degree_in v_v ) = 1"
1.24 ]),
1.25 - ("#Find" ,["solutions v_i"])
1.26 + ("#Find" ,["solutions v_i'''"])
1.27 ],
1.28 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
1.29 [["PolyEq","solve_d1_polyeq_equation"]]));
1.30 @@ -890,7 +890,7 @@
1.31 ("#Where" ,["matches (?a = 0) e_e",
1.32 "(lhs e_e) is_poly_in v_v ",
1.33 "((lhs e_e) has_degree_in v_v ) = 2"]),
1.34 - ("#Find" ,["solutions v_i"])
1.35 + ("#Find" ,["solutions v_i'''"])
1.36 ],
1.37 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
1.38 [["PolyEq","solve_d2_polyeq_equation"]]));
1.39 @@ -911,7 +911,7 @@
1.40 "Not (matches ( ?b*?v_ + ?v_^^^2 = 0) e_e) &" ^
1.41 "Not (matches ( ?v_ + ?c*?v_^^^2 = 0) e_e) &" ^
1.42 "Not (matches ( ?b*?v_ + ?c*?v_^^^2 = 0) e_e)"]),
1.43 - ("#Find" ,["solutions v_i"])
1.44 + ("#Find" ,["solutions v_i'''"])
1.45 ],
1.46 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
1.47 [["PolyEq","solve_d2_polyeq_sqonly_equation"]]));
1.48 @@ -926,7 +926,7 @@
1.49 "matches (?a*?v_ + ?b*?v_^^^2 = 0) e_e | " ^
1.50 "matches ( ?v_^^^2 = 0) e_e | " ^
1.51 "matches ( ?b*?v_^^^2 = 0) e_e "]),
1.52 - ("#Find" ,["solutions v_i"])
1.53 + ("#Find" ,["solutions v_i'''"])
1.54 ],
1.55 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
1.56 [["PolyEq","solve_d2_polyeq_bdvonly_equation"]]));
1.57 @@ -937,7 +937,7 @@
1.58 [("#Given" ,["equality e_e","solveFor v_v"]),
1.59 ("#Where" ,["matches (?a + 1*?v_^^^2 = 0) e_e | " ^
1.60 "matches (?a + ?v_^^^2 = 0) e_e"]),
1.61 - ("#Find" ,["solutions v_i"])
1.62 + ("#Find" ,["solutions v_i'''"])
1.63 ],
1.64 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
1.65 [["PolyEq","solve_d2_polyeq_pq_equation"]]));
1.66 @@ -948,7 +948,7 @@
1.67 [("#Given" ,["equality e_e","solveFor v_v"]),
1.68 ("#Where" ,["matches (?a + ?v_^^^2 = 0) e_e | " ^
1.69 "matches (?a + ?b*?v_^^^2 = 0) e_e"]),
1.70 - ("#Find" ,["solutions v_i"])
1.71 + ("#Find" ,["solutions v_i'''"])
1.72 ],
1.73 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
1.74 [["PolyEq","solve_d2_polyeq_abc_equation"]]));
1.75 @@ -962,7 +962,7 @@
1.76 ("#Where" ,["matches (?a = 0) e_e",
1.77 "(lhs e_e) is_poly_in v_v ",
1.78 "((lhs e_e) has_degree_in v_v) = 3"]),
1.79 - ("#Find" ,["solutions v_i"])
1.80 + ("#Find" ,["solutions v_i'''"])
1.81 ],
1.82 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
1.83 [["PolyEq","solve_d3_polyeq_equation"]]));
1.84 @@ -975,7 +975,7 @@
1.85 ("#Where" ,["matches (?a = 0) e_e",
1.86 "(lhs e_e) is_poly_in v_v ",
1.87 "((lhs e_e) has_degree_in v_v) = 4"]),
1.88 - ("#Find" ,["solutions v_i"])
1.89 + ("#Find" ,["solutions v_i'''"])
1.90 ],
1.91 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
1.92 [(*["PolyEq","solve_d4_polyeq_equation"]*)]));
1.93 @@ -987,7 +987,7 @@
1.94 [("#Given" ,["equality e_e","solveFor v_v"]),
1.95 ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) |" ^
1.96 "(Not(((lhs e_e) is_poly_in v_v)))"]),
1.97 - ("#Find" ,["solutions v_i"])
1.98 + ("#Find" ,["solutions v_i'''"])
1.99 ],
1.100 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
1.101 [["PolyEq","normalize_poly"]]));
1.102 @@ -998,7 +998,7 @@
1.103 [("#Given" ,["equality e_e","solveFor v_v"]),
1.104 ("#Where" ,["matches (?a = 0) e_e",
1.105 "(lhs e_e) is_expanded_in v_v "]),
1.106 - ("#Find" ,["solutions v_i"])
1.107 + ("#Find" ,["solutions v_i'''"])
1.108 ],
1.109 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
1.110 []));
1.111 @@ -1009,7 +1009,7 @@
1.112 (["degree_2","expanded","univariate","equation"],
1.113 [("#Given" ,["equality e_e","solveFor v_v"]),
1.114 ("#Where" ,["((lhs e_e) has_degree_in v_v) = 2"]),
1.115 - ("#Find" ,["solutions v_i"])
1.116 + ("#Find" ,["solutions v_i'''"])
1.117 ],
1.118 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
1.119 [["PolyEq","complete_square"]]));
1.120 @@ -1043,7 +1043,7 @@
1.121 [("#Given" ,["equality e_e","solveFor v_v"]),
1.122 ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) |" ^
1.123 "(Not(((lhs e_e) is_poly_in v_v)))"]),
1.124 - ("#Find" ,["solutions v_i"])
1.125 + ("#Find" ,["solutions v_i'''"])
1.126 ],
1.127 {rew_ord'="termlessI",
1.128 rls'=PolyEq_erls,
1.129 @@ -1070,7 +1070,7 @@
1.130 [("#Given" ,["equality e_e","solveFor v_v"]),
1.131 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
1.132 "((lhs e_e) has_degree_in v_v) = 0"]),
1.133 - ("#Find" ,["solutions v_i"])
1.134 + ("#Find" ,["solutions v_i'''"])
1.135 ],
1.136 {rew_ord'="termlessI",
1.137 rls'=PolyEq_erls,
1.138 @@ -1091,7 +1091,7 @@
1.139 [("#Given" ,["equality e_e","solveFor v_v"]),
1.140 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
1.141 "((lhs e_e) has_degree_in v_v) = 1"]),
1.142 - ("#Find" ,["solutions v_i"])
1.143 + ("#Find" ,["solutions v_i'''"])
1.144 ],
1.145 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
1.146 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
1.147 @@ -1112,7 +1112,7 @@
1.148 [("#Given" ,["equality e_e","solveFor v_v"]),
1.149 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
1.150 "((lhs e_e) has_degree_in v_v) = 2"]),
1.151 - ("#Find" ,["solutions v_i"])
1.152 + ("#Find" ,["solutions v_i'''"])
1.153 ],
1.154 {rew_ord'="termlessI",
1.155 rls'=PolyEq_erls,
1.156 @@ -1139,7 +1139,7 @@
1.157 [("#Given" ,["equality e_e","solveFor v_v"]),
1.158 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
1.159 "((lhs e_e) has_degree_in v_v) = 2"]),
1.160 - ("#Find" ,["solutions v_i"])
1.161 + ("#Find" ,["solutions v_i'''"])
1.162 ],
1.163 {rew_ord'="termlessI",
1.164 rls'=PolyEq_erls,
1.165 @@ -1166,7 +1166,7 @@
1.166 [("#Given" ,["equality e_e","solveFor v_v"]),
1.167 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
1.168 "((lhs e_e) has_degree_in v_v) = 2"]),
1.169 - ("#Find" ,["solutions v_i"])
1.170 + ("#Find" ,["solutions v_i'''"])
1.171 ],
1.172 {rew_ord'="termlessI",
1.173 rls'=PolyEq_erls,
1.174 @@ -1190,7 +1190,7 @@
1.175 [("#Given" ,["equality e_e","solveFor v_v"]),
1.176 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
1.177 "((lhs e_e) has_degree_in v_v) = 2"]),
1.178 - ("#Find" ,["solutions v_i"])
1.179 + ("#Find" ,["solutions v_i'''"])
1.180 ],
1.181 {rew_ord'="termlessI",
1.182 rls'=PolyEq_erls,
1.183 @@ -1214,7 +1214,7 @@
1.184 [("#Given" ,["equality e_e","solveFor v_v"]),
1.185 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
1.186 "((lhs e_e) has_degree_in v_v) = 2"]),
1.187 - ("#Find" ,["solutions v_i"])
1.188 + ("#Find" ,["solutions v_i'''"])
1.189 ],
1.190 {rew_ord'="termlessI",
1.191 rls'=PolyEq_erls,
1.192 @@ -1238,7 +1238,7 @@
1.193 [("#Given" ,["equality e_e","solveFor v_v"]),
1.194 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
1.195 "((lhs e_e) has_degree_in v_v) = 3"]),
1.196 - ("#Find" ,["solutions v_i"])
1.197 + ("#Find" ,["solutions v_i'''"])
1.198 ],
1.199 {rew_ord'="termlessI",
1.200 rls'=PolyEq_erls,
1.201 @@ -1271,7 +1271,7 @@
1.202 [("#Given" ,["equality e_e","solveFor v_v"]),
1.203 ("#Where" ,["matches (?a = 0) e_e",
1.204 "((lhs e_e) has_degree_in v_v) = 2"]),
1.205 - ("#Find" ,["solutions v_i"])
1.206 + ("#Find" ,["solutions v_i'''"])
1.207 ],
1.208 {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
1.209 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],